Theorem rabid2 3118

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 2732	. . 3 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
2		pm4.71 662	. . . 4 |- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
3	2	albii 1747	. . 3 |- ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
4	1, 3	bitr4i 267	. 2 |- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A -> ph ) )
5		df-rab 2921	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i 2634	. 2 |- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral 2917	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
8	4, 6, 7	3bitr4i 292	1 |- ( A = { x e. A | ph } <-> A. x e. A ph )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   {crab 2916

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-ral 2917  df-rab 2921

This theorem is referenced by:  rabxm  3961  iinrab2  4583  riinrab  4596  class2seteq  4833  dmmptg  5632  wfisg  5715  dmmptd  6024  fneqeql  6325  fmpt  6381  zfrep6  7134  axdc2lem  9270  ioomax  12248  iccmax  12249  hashbc  13237  lcmf0  15347  dfphi2  15479  phiprmpw  15481  phisum  15495  isnsg4  17637  symggen2  17891  psgnfvalfi  17933  lssuni  18940  psr1baslem  19555  psgnghm2  19927  ocv0  20021  dsmmfi  20082  frlmfibas  20105  frlmlbs  20136  ordtrest2lem  21007  comppfsc  21335  xkouni  21402  xkoccn  21422  tsmsfbas  21931  clsocv  23049  ehlbase  23194  ovolicc2lem4  23288  itg2monolem1  23517  musum  24917  lgsquadlem2  25106  umgr2v2evd2  26423  frgrregorufr0  27188  ubthlem1  27726  xrsclat  29680  psgndmfi  29846  ordtrest2NEWlem  29968  hasheuni  30147  measvuni  30277  imambfm  30324  subfacp1lem6  31167  connpconn  31217  cvmliftmolem2  31264  cvmlift2lem12  31296  tfisg  31716  frinsg  31742  poimirlem28  33437  fdc  33541  isbnd3  33583  pmap1N  35053  pol1N  35196  dia1N  36342  dihwN  36578  vdioph  37343  fiphp3d  37383  dmmptdf  39417  stirlinglem14  40304  suppdm  42300