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	|- ( ph -> A =/= (/) )
	iinexd.2	|- ( ph -> A. x e. A B e. C )
Assertion	iinexd	|- ( ph -> |^|_ x e. A B e. _V )

Proof

Step	Hyp	Ref	Expression
1		iinexd.1	|- ( ph -> A =/= (/) )
2		iinexd.2	|- ( ph -> A. x e. A B e. C )
3		iinexg	|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^|_ x e. A B e. _V )
4	1 2 3	syl2anc	|- ( ph -> |^|_ x e. A B e. _V )