Theorem rabid2 2664

Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rabid2	|- ( A = { x e. A | ph } <-> A. x e. A ph )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem rabid2

Step	Hyp	Ref	Expression
1		abeq2 2296	. . 3 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
2		pm4.71 389	. . . 4 |- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
3	2	albii 1480	. . 3 |- ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
4	1, 3	bitr4i 187	. 2 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A -> ph ) )
5		df-rab 2474	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i 2198	. 2 |- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral 2470	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
8	4, 6, 7	3bitr4i 212	1 |- ( A = { x e. A | ph } <-> A. x e. A ph )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1361   = wceq 1363   e. wcel 2158   {cab 2173   A.wral 2465   {crab 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-ral 2470  df-rab 2474

This theorem is referenced by:  rabxmdc  3466  rabrsndc  3672  class2seteq  4175  dmmptg  5138  dmmptd  5358  fneqeql  5637  fmpt  5679  acexmidlemph  5881  inffiexmid  6919  ssfirab  6946  exmidaclem  7220  ioomax  9961  iccmax  9962  dfphi2  12233  phiprmpw  12235  phisum  12253  unennn  12411  znnen  12412  isnsg4  13103  lssuni  13547