This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinexd

Description: The existence of an indexed union. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	iinexd.1	$⊢ φ \to A \neq \emptyset$
	iinexd.2	$⊢ φ \to \forall x \in A B \in C$
Assertion	iinexd	$⊢ φ \to ⋂_{x \in A} B \in V$

Proof

Step	Hyp	Ref	Expression
1		iinexd.1	$⊢ φ \to A \neq \emptyset$
2		iinexd.2	$⊢ φ \to \forall x \in A B \in C$
3		iinexg	$⊢ (A \neq \emptyset \land \forall x \in A B \in C) \to ⋂_{x \in A} B \in V$
4	1 2 3	syl2anc	$⊢ φ \to ⋂_{x \in A} B \in V$