Theorem rabid2 3445

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∀wral 3077  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rab 3414

This theorem is used by:  iinrab2  5028  riinrab  5044  dmmptg  6243  frpoinsg  6346  dmmptd  6684  fneqeql  7045  fmpt  7110  tfisg  7865  zfrep6OLD  7967  frinsg  9755  axdc2lem  10526  ioomax  13553  iccmax  13554  hashbc  14598  lcmf0  16809  dfphi2  16951  phiprmpw  16953  phisum  16968  isnsg4  19377  symggen2  19685  psgnfvalfi  19727  lssuni  21214  psgnghm2  21887  ocv0  21983  dsmmfi  22044  frlmfibas  22068  frlmlbs  22103  psr1baslem  22503  ordtrest2lem  23521  comppfsc  23851  xkouni  23918  xkoccn  23938  tsmsfbas  24447  clsocv  25571  ehlbase  25736  ovolicc2lem4  25841  itg2monolem1  26071  musum  27518  lgsquadlem2  27708  umgr2v2evd2  30108  frgrregorufr0  30925  ubthlem1  31472  xrsclat  33572  psgndmfi  33659  primefldgen1  33883  zarcls0  34500  ordtrest2NEWlem  34554  hasheuni  34717  measvuni  34847  imambfm  34894  subfacp1lem6  35950  connpconn  36000  cvmliftmolem2  36047  cvmlift2lem12  36079  poimirlem28  38566  fdc  38679  isbnd3  38718  pmap1N  40824  pol1N  40967  dia1N  42110  dihwN  42346  vdioph  43789  fiphp3d  43825  stirlinglem14  47096  fvmptrabdm  48362  suppdm  49621