Theorem eluni2f

Description: Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	eluni2f.1	|- F/_ x A
	eluni2f.2	|- F/_ x B
Assertion	eluni2f	|- ( A e. U. B <-> E. x e. B A e. x )

Proof

Step	Hyp	Ref	Expression
1		eluni2f.1	|- F/_ x A
2		eluni2f.2	|- F/_ x B
3		exancom	|- ( E. x ( A e. x /\ x e. B ) <-> E. x ( x e. B /\ A e. x ) )
4	1 2	elunif	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )
5		df-rex	|- ( E. x e. B A e. x <-> E. x ( x e. B /\ A e. x ) )
6	3 4 5	3bitr4i	|- ( A e. U. B <-> E. x e. B A e. x )