Theorem eluni

Description: Membership in class union. (Contributed by NM, 22-May-1994)

	Ref	Expression
Assertion	eluni	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. U. B -> A e. _V )
2		elex	|- ( A e. x -> A e. _V )
3	2	adantr	|- ( ( A e. x /\ x e. B ) -> A e. _V )
4	3	exlimiv	|- ( E. x ( A e. x /\ x e. B ) -> A e. _V )
5		eleq1	|- ( y = A -> ( y e. x <-> A e. x ) )
6	5	anbi1d	|- ( y = A -> ( ( y e. x /\ x e. B ) <-> ( A e. x /\ x e. B ) ) )
7	6	exbidv	|- ( y = A -> ( E. x ( y e. x /\ x e. B ) <-> E. x ( A e. x /\ x e. B ) ) )
8		df-uni	|- U. B = { y | E. x ( y e. x /\ x e. B ) }
9	7 8	elab2g	|- ( A e. _V -> ( A e. U. B <-> E. x ( A e. x /\ x e. B ) ) )
10	1 4 9	pm5.21nii	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )