Theorem rabid2 3434

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

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

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 3402

This theorem is referenced by:  iinrab2  5027  riinrab  5041  dmmptg  6208  frpoinsg  6309  dmmptd  6645  fneqeql  7000  fmpt  7064  tfisg  7806  zfrep6  7909  frinsg  9675  axdc2lem  10370  ioomax  13350  iccmax  13351  hashbc  14388  lcmf0  16573  dfphi2  16713  phiprmpw  16715  phisum  16730  isnsg4  19111  symggen2  19415  psgnfvalfi  19457  lssuni  20905  psgnghm2  21551  ocv0  21647  dsmmfi  21708  frlmfibas  21732  frlmlbs  21767  psr1baslem  22140  ordtrest2lem  23162  comppfsc  23491  xkouni  23558  xkoccn  23578  tsmsfbas  24087  clsocv  25221  ehlbase  25386  ovolicc2lem4  25492  itg2monolem1  25722  musum  27172  lgsquadlem2  27363  umgr2v2evd2  29617  frgrregorufr0  30415  ubthlem1  30962  xrsclat  33108  psgndmfi  33196  primefldgen1  33419  zarcls0  34050  ordtrest2NEWlem  34104  hasheuni  34267  measvuni  34396  imambfm  34444  subfacp1lem6  35405  connpconn  35455  cvmliftmolem2  35502  cvmlift2lem12  35534  poimirlem28  37903  fdc  38000  isbnd3  38039  pmap1N  40147  pol1N  40290  dia1N  41433  dihwN  41669  vdioph  43140  fiphp3d  43180  stirlinglem14  46449  fvmptrabdm  47657  suppdm  48874