Theorem eluniab

Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	eluniab	|- ( A e. U. { x | ph } <-> E. x ( A e. x /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		eluni	|- ( A e. U. { x | ph } <-> E. y ( A e. y /\ y e. { x | ph } ) )
2		nfv	|- F/ x A e. y
3		nfsab1	|- F/ x y e. { x | ph }
4	2 3	nfan	|- F/ x ( A e. y /\ y e. { x | ph } )
5		nfv	|- F/ y ( A e. x /\ ph )
6		eleq2w	|- ( y = x -> ( A e. y <-> A e. x ) )
7		eleq1w	|- ( y = x -> ( y e. { x | ph } <-> x e. { x | ph } ) )
8		abid	|- ( x e. { x | ph } <-> ph )
9	7 8	bitrdi	|- ( y = x -> ( y e. { x | ph } <-> ph ) )
10	6 9	anbi12d	|- ( y = x -> ( ( A e. y /\ y e. { x | ph } ) <-> ( A e. x /\ ph ) ) )
11	4 5 10	cbvexv1	|- ( E. y ( A e. y /\ y e. { x | ph } ) <-> E. x ( A e. x /\ ph ) )
12	1 11	bitri	|- ( A e. U. { x | ph } <-> E. x ( A e. x /\ ph ) )