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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∀wral 3080  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rab 3417

This theorem is used by:  iinrab2  5031  riinrab  5047  dmmptg  6250  frpoinsg  6353  dmmptd  6695  fneqeql  7056  fmpt  7121  tfisg  7875  zfrep6OLD  7977  frinsg  9768  axdc2lem  10539  ioomax  13566  iccmax  13567  hashbc  14611  lcmf0  16824  dfphi2  16966  phiprmpw  16968  phisum  16983  isnsg4  19392  symggen2  19700  psgnfvalfi  19742  lssuni  21229  psgnghm2  21902  ocv0  21998  dsmmfi  22059  frlmfibas  22083  frlmlbs  22118  psr1baslem  22518  ordtrest2lem  23536  comppfsc  23866  xkouni  23933  xkoccn  23953  tsmsfbas  24462  clsocv  25586  ehlbase  25751  ovolicc2lem4  25856  itg2monolem1  26086  musum  27533  lgsquadlem2  27723  umgr2v2evd2  30123  frgrregorufr0  30940  ubthlem1  31487  xrsclat  33628  psgndmfi  33715  primefldgen1  33939  zarcls0  34556  ordtrest2NEWlem  34610  hasheuni  34773  measvuni  34903  imambfm  34950  subfacp1lem6  36074  connpconn  36124  cvmliftmolem2  36171  cvmlift2lem12  36203  poimirlem28  38709  fdc  38822  isbnd3  38861  pmap1N  40967  pol1N  41110  dia1N  42253  dihwN  42489  vdioph  43933  fiphp3d  43969  stirlinglem14  47239  fvmptrabdm  48505  suppdm  49764