Theorem rabid2 3456

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

Syntax hints:   ↔ wb 209   = wceq 1567  ∀wral 3085  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rab 3424

This theorem is referenced by:  iinrab2  5038  riinrab  5054  dmmptg  6244  frpoinsg  6345  dmmptd  6681  fneqeql  7042  fmpt  7106  tfisg  7850  zfrep6OLD  7952  frinsg  9723  axdc2lem  10432  ioomax  13449  iccmax  13450  hashbc  14490  lcmf0  16692  dfphi2  16833  phiprmpw  16835  phisum  16850  isnsg4  19233  symggen2  19541  psgnfvalfi  19583  lssuni  21038  psgnghm2  21700  ocv0  21796  dsmmfi  21857  frlmfibas  21881  frlmlbs  21916  psr1baslem  22314  ordtrest2lem  23329  comppfsc  23658  xkouni  23725  xkoccn  23745  tsmsfbas  24254  clsocv  25378  ehlbase  25543  ovolicc2lem4  25648  itg2monolem1  25878  musum  27321  lgsquadlem2  27511  umgr2v2evd2  29818  frgrregorufr0  30616  ubthlem1  31163  xrsclat  33272  psgndmfi  33359  primefldgen1  33585  zarcls0  34203  ordtrest2NEWlem  34257  hasheuni  34420  measvuni  34549  imambfm  34597  subfacp1lem6  35610  connpconn  35660  cvmliftmolem2  35707  cvmlift2lem12  35739  poimirlem28  38221  fdc  38318  isbnd3  38357  pmap1N  40465  pol1N  40608  dia1N  41751  dihwN  41987  vdioph  43436  fiphp3d  43472  stirlinglem14  46727  fvmptrabdm  47953  suppdm  49209