Theorem rabid2 3428

Description: An "identity" law for restricted class abstraction. Prefer rabid2im 3427 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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3426	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1540  ∀wral 3044  {crab 3394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3395

This theorem is referenced by:  iinrab2  5019  riinrab  5033  dmmptg  6191  frpoinsg  6291  dmmptd  6627  fneqeql  6980  fmpt  7044  tfisg  7787  zfrep6  7890  frinsg  9647  axdc2lem  10342  ioomax  13325  iccmax  13326  hashbc  14360  lcmf0  16545  dfphi2  16685  phiprmpw  16687  phisum  16702  isnsg4  19046  symggen2  19350  psgnfvalfi  19392  lssuni  20842  psgnghm2  21488  ocv0  21584  dsmmfi  21645  frlmfibas  21669  frlmlbs  21704  psr1baslem  22067  ordtrest2lem  23088  comppfsc  23417  xkouni  23484  xkoccn  23504  tsmsfbas  24013  clsocv  25148  ehlbase  25313  ovolicc2lem4  25419  itg2monolem1  25649  musum  27099  lgsquadlem2  27290  umgr2v2evd2  29473  frgrregorufr0  30268  ubthlem1  30814  xrsclat  32966  psgndmfi  33041  primefldgen1  33261  zarcls0  33841  ordtrest2NEWlem  33895  hasheuni  34058  measvuni  34187  imambfm  34236  subfacp1lem6  35168  connpconn  35218  cvmliftmolem2  35265  cvmlift2lem12  35297  poimirlem28  37638  fdc  37735  isbnd3  37774  pmap1N  39756  pol1N  39899  dia1N  41042  dihwN  41278  vdioph  42762  fiphp3d  42802  stirlinglem14  46078  fvmptrabdm  47287  suppdm  48505