Theorem rabid2 3437

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

Assertion

Ref	Expression
rabid2	⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabid2

Step	Hyp	Ref	Expression
1		nfcv 2902	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3436	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1541  ∀wral 3060  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rab 3406

This theorem is referenced by:  class2seteq  3665  rabxm  4351  iinrab2  5035  riinrab  5049  dmmptg  6199  frpoinsg  6302  wfisgOLD  6313  dmmptd  6651  fneqeql  7001  fmpt  7063  tfisg  7795  zfrep6  7892  frinsg  9696  axdc2lem  10393  ioomax  13349  iccmax  13350  hashbc  14362  lcmf0  16521  dfphi2  16657  phiprmpw  16659  phisum  16673  isnsg4  18983  symggen2  19267  psgnfvalfi  19309  lssuni  20457  psgnghm2  21022  ocv0  21118  dsmmfi  21181  frlmfibas  21205  frlmlbs  21240  psr1baslem  21593  ordtrest2lem  22591  comppfsc  22920  xkouni  22987  xkoccn  23007  tsmsfbas  23516  clsocv  24651  ehlbase  24816  ovolicc2lem4  24921  itg2monolem1  25152  musum  26577  lgsquadlem2  26766  umgr2v2evd2  28538  frgrregorufr0  29331  ubthlem1  29875  xrsclat  31941  psgndmfi  32017  primefldgen1  32159  zarcls0  32538  ordtrest2NEWlem  32592  hasheuni  32773  measvuni  32902  imambfm  32951  subfacp1lem6  33866  connpconn  33916  cvmliftmolem2  33963  cvmlift2lem12  33995  poimirlem28  36179  fdc  36277  isbnd3  36316  pmap1N  38303  pol1N  38446  dia1N  39589  dihwN  39825  vdioph  41160  fiphp3d  41200  stirlinglem14  44448  fvmptrabdm  45645  suppdm  46711