Theorem rabid2 3433

Description: An "identity" law for restricted class abstraction. Prefer rabid2im 3432 if one direction is sufficient. (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 2899	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3431	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1542  ∀wral 3052  {crab 3400

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rab 3401

This theorem is referenced by:  iinrab2  5026  riinrab  5040  dmmptg  6201  frpoinsg  6302  dmmptd  6638  fneqeql  6993  fmpt  7057  tfisg  7798  zfrep6  7901  frinsg  9667  axdc2lem  10362  ioomax  13342  iccmax  13343  hashbc  14380  lcmf0  16565  dfphi2  16705  phiprmpw  16707  phisum  16722  isnsg4  19100  symggen2  19404  psgnfvalfi  19446  lssuni  20894  psgnghm2  21540  ocv0  21636  dsmmfi  21697  frlmfibas  21721  frlmlbs  21756  psr1baslem  22129  ordtrest2lem  23151  comppfsc  23480  xkouni  23547  xkoccn  23567  tsmsfbas  24076  clsocv  25210  ehlbase  25375  ovolicc2lem4  25481  itg2monolem1  25711  musum  27161  lgsquadlem2  27352  umgr2v2evd2  29584  frgrregorufr0  30382  ubthlem1  30928  xrsclat  33074  psgndmfi  33161  primefldgen1  33384  zarcls0  34006  ordtrest2NEWlem  34060  hasheuni  34223  measvuni  34352  imambfm  34400  subfacp1lem6  35360  connpconn  35410  cvmliftmolem2  35457  cvmlift2lem12  35489  poimirlem28  37820  fdc  37917  isbnd3  37956  pmap1N  40064  pol1N  40207  dia1N  41350  dihwN  41586  vdioph  43057  fiphp3d  43097  stirlinglem14  46367  fvmptrabdm  47575  suppdm  48792