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		elequ1	|- ( y = z -> ( y e. x <-> z e. x ) )
6	5	anbi1d	|- ( y = z -> ( ( y e. x /\ x e. B ) <-> ( z e. x /\ x e. B ) ) )
7	6	exbidv	|- ( y = z -> ( E. x ( y e. x /\ x e. B ) <-> E. x ( z e. x /\ x e. B ) ) )
8		eleq1	|- ( z = A -> ( z e. x <-> A e. x ) )
9	8	anbi1d	|- ( z = A -> ( ( z e. x /\ x e. B ) <-> ( A e. x /\ x e. B ) ) )
10	9	exbidv	|- ( z = A -> ( E. x ( z e. x /\ x e. B ) <-> E. x ( A e. x /\ x e. B ) ) )
11		df-uni	|- U. B = { y | E. x ( y e. x /\ x e. B ) }
12	7 10 11	elab2gw	|- ( A e. _V -> ( A e. U. B <-> E. x ( A e. x /\ x e. B ) ) )
13	1 4 12	pm5.21nii	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )