I'm wondering what the following statement is equivalent to in an intuitionistic framework.
For a union of sets $C = \bigcup\limits_{i \in I} X_i,$ if $S \in C,$ there exists $s \in I$ such that $S \in X_s.$
In classical logic, the proof just relies on ZF and the law of the excluded middle. Indeed, if there does not exist $s$ such that $S \in X_s,$ then $S \not\in X_s$ for all $s \in I,$ hence $S \not\in C$ by the definition of union, contradiction.
As best I can tell, it's not so much an important axiom or theorem as the definition of $\bigcup$ (or rather it would be, if you changed the if to iff). As it stands, it follows from the iff version of the definition.