Theorem rabid2 3448

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

Syntax hints:   ↔ wb 208   = wceq 1561  ∀wral 3077  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-nf 1805  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3078  df-rab 3416

This theorem is referenced by:  iinrab2  5028  riinrab  5042  dmmptg  6230  frpoinsg  6331  dmmptd  6667  fneqeql  7028  fmpt  7092  tfisg  7835  zfrep6OLD  7937  frinsg  9710  axdc2lem  10406  ioomax  13427  iccmax  13428  hashbc  14467  lcmf0  16669  dfphi2  16810  phiprmpw  16812  phisum  16827  isnsg4  19209  symggen2  19512  psgnfvalfi  19554  lssuni  21007  psgnghm2  21634  ocv0  21730  dsmmfi  21791  frlmfibas  21815  frlmlbs  21850  psr1baslem  22248  ordtrest2lem  23264  comppfsc  23593  xkouni  23660  xkoccn  23680  tsmsfbas  24189  clsocv  25313  ehlbase  25478  ovolicc2lem4  25583  itg2monolem1  25813  musum  27256  lgsquadlem2  27446  umgr2v2evd2  29729  frgrregorufr0  30527  ubthlem1  31074  xrsclat  33190  psgndmfi  33279  primefldgen1  33509  zarcls0  34166  ordtrest2NEWlem  34220  hasheuni  34383  measvuni  34512  imambfm  34560  subfacp1lem6  35536  connpconn  35586  cvmliftmolem2  35633  cvmlift2lem12  35665  poimirlem28  38148  fdc  38245  isbnd3  38284  pmap1N  40392  pol1N  40535  dia1N  41678  dihwN  41914  vdioph  43361  fiphp3d  43397  stirlinglem14  46662  fvmptrabdm  47888  suppdm  49133