Theorem rabid2 3465

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 2904	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3464	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1542  ∀wral 3062  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rab 3434

This theorem is referenced by:  class2seteq  3699  rabxm  4385  iinrab2  5072  riinrab  5086  dmmptg  6238  frpoinsg  6341  wfisgOLD  6352  dmmptd  6692  fneqeql  7043  fmpt  7105  tfisg  7838  zfrep6  7936  frinsg  9742  axdc2lem  10439  ioomax  13395  iccmax  13396  hashbc  14408  lcmf0  16567  dfphi2  16703  phiprmpw  16705  phisum  16719  isnsg4  19041  symggen2  19332  psgnfvalfi  19374  lssuni  20538  psgnghm2  21118  ocv0  21214  dsmmfi  21277  frlmfibas  21301  frlmlbs  21336  psr1baslem  21691  ordtrest2lem  22689  comppfsc  23018  xkouni  23085  xkoccn  23105  tsmsfbas  23614  clsocv  24749  ehlbase  24914  ovolicc2lem4  25019  itg2monolem1  25250  musum  26675  lgsquadlem2  26864  umgr2v2evd2  28764  frgrregorufr0  29557  ubthlem1  30101  xrsclat  32159  psgndmfi  32235  primefldgen1  32380  zarcls0  32786  ordtrest2NEWlem  32840  hasheuni  33021  measvuni  33150  imambfm  33199  subfacp1lem6  34114  connpconn  34164  cvmliftmolem2  34211  cvmlift2lem12  34243  poimirlem28  36454  fdc  36551  isbnd3  36590  pmap1N  38576  pol1N  38719  dia1N  39862  dihwN  40098  vdioph  41450  fiphp3d  41490  stirlinglem14  44738  fvmptrabdm  45936  suppdm  47093