Theorem rabid2 3423

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

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

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 3391

This theorem is referenced by:  iinrab2  5013  riinrab  5027  dmmptg  6202  frpoinsg  6303  dmmptd  6639  fneqeql  6994  fmpt  7058  tfisg  7800  zfrep6OLD  7903  frinsg  9670  axdc2lem  10365  ioomax  13370  iccmax  13371  hashbc  14410  lcmf0  16598  dfphi2  16739  phiprmpw  16741  phisum  16756  isnsg4  19137  symggen2  19441  psgnfvalfi  19483  lssuni  20929  psgnghm2  21575  ocv0  21671  dsmmfi  21732  frlmfibas  21756  frlmlbs  21791  psr1baslem  22162  ordtrest2lem  23182  comppfsc  23511  xkouni  23578  xkoccn  23598  tsmsfbas  24107  clsocv  25231  ehlbase  25396  ovolicc2lem4  25501  itg2monolem1  25731  musum  27172  lgsquadlem2  27362  umgr2v2evd2  29615  frgrregorufr0  30413  ubthlem1  30960  xrsclat  33090  psgndmfi  33178  primefldgen1  33401  zarcls0  34032  ordtrest2NEWlem  34086  hasheuni  34249  measvuni  34378  imambfm  34426  subfacp1lem6  35387  connpconn  35437  cvmliftmolem2  35484  cvmlift2lem12  35516  poimirlem28  37987  fdc  38084  isbnd3  38123  pmap1N  40231  pol1N  40374  dia1N  41517  dihwN  41753  vdioph  43229  fiphp3d  43269  stirlinglem14  46537  fvmptrabdm  47757  suppdm  49002