Theorem rabid2 3312

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∀wral 3065  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rab 3074

This theorem is referenced by:  rabxm  4325  iinrab2  5003  riinrab  5017  class2seteq  5280  dmmptg  6142  frpoinsg  6243  wfisgOLD  6254  dmmptd  6574  fneqeql  6917  fmpt  6978  zfrep6  7784  frinsg  9493  axdc2lem  10188  ioomax  13136  iccmax  13137  hashbc  14146  lcmf0  16320  dfphi2  16456  phiprmpw  16458  phisum  16472  isnsg4  18776  symggen2  19060  psgnfvalfi  19102  lssuni  20182  psgnghm2  20767  ocv0  20863  dsmmfi  20926  frlmfibas  20950  frlmlbs  20985  psr1baslem  21337  ordtrest2lem  22335  comppfsc  22664  xkouni  22731  xkoccn  22751  tsmsfbas  23260  clsocv  24395  ehlbase  24560  ovolicc2lem4  24665  itg2monolem1  24896  musum  26321  lgsquadlem2  26510  umgr2v2evd2  27875  frgrregorufr0  28667  ubthlem1  29211  xrsclat  31268  psgndmfi  31344  zarcls0  31797  ordtrest2NEWlem  31851  hasheuni  32032  measvuni  32161  imambfm  32208  subfacp1lem6  33126  connpconn  33176  cvmliftmolem2  33223  cvmlift2lem12  33255  tfisg  33765  poimirlem28  35784  fdc  35882  isbnd3  35921  pmap1N  37760  pol1N  37903  dia1N  39046  dihwN  39282  vdioph  40581  fiphp3d  40621  dmmptdf  42716  stirlinglem14  43582  fvmptrabdm  44736  suppdm  45803