Theorem eluniab 4447

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

Assertion

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

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem eluniab

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni 4439	. 2 |- ( A e. U. { x | ph } <-> E. y ( A e. y /\ y e. { x | ph } ) )
2		nfv 1843	. . . 4 |- F/ x A e. y
3		nfsab1 2612	. . . 4 |- F/ x y e. { x | ph }
4	2, 3	nfan 1828	. . 3 |- F/ x ( A e. y /\ y e. { x | ph } )
5		nfv 1843	. . 3 |- F/ y ( A e. x /\ ph )
6		eleq2 2690	. . . 4 |- ( y = x -> ( A e. y <-> A e. x ) )
7		eleq1 2689	. . . . 5 |- ( y = x -> ( y e. { x | ph } <-> x e. { x | ph } ) )
8		abid 2610	. . . . 5 |- ( x e. { x | ph } <-> ph )
9	7, 8	syl6bb 276	. . . 4 |- ( y = x -> ( y e. { x | ph } <-> ph ) )
10	6, 9	anbi12d 747	. . 3 |- ( y = x -> ( ( A e. y /\ y e. { x | ph } ) <-> ( A e. x /\ ph ) ) )
11	4, 5, 10	cbvex 2272	. 2 |- ( E. y ( A e. y /\ y e. { x | ph } ) <-> E. x ( A e. x /\ ph ) )
12	1, 11	bitri 264	1 |- ( A e. U. { x | ph } <-> E. x ( A e. x /\ ph ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704   e. wcel 1990   {cab 2608   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-uni 4437

This theorem is referenced by:  elunirab  4448  dfiun2g  4552  inuni  4826  elfv  6189  snnexOLD  6967  unielxp  7204  wfrlem12  7426  tfrlem9  7481  dfac5lem2  8947  fin23lem30  9164  unisngl  21330  metrest  22329  aannenlem2  24084  fpwrelmapffslem  29507  frrlem11  31792  dfiota3  32030  mptsnunlem  33185