Theorem rabid2 3430

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∀wral 3049  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rab 3398

This theorem is referenced by:  iinrab2  5023  riinrab  5037  dmmptg  6198  frpoinsg  6299  dmmptd  6635  fneqeql  6989  fmpt  7053  tfisg  7794  zfrep6  7897  frinsg  9661  axdc2lem  10356  ioomax  13336  iccmax  13337  hashbc  14374  lcmf0  16559  dfphi2  16699  phiprmpw  16701  phisum  16716  isnsg4  19094  symggen2  19398  psgnfvalfi  19440  lssuni  20888  psgnghm2  21534  ocv0  21630  dsmmfi  21691  frlmfibas  21715  frlmlbs  21750  psr1baslem  22123  ordtrest2lem  23145  comppfsc  23474  xkouni  23541  xkoccn  23561  tsmsfbas  24070  clsocv  25204  ehlbase  25369  ovolicc2lem4  25475  itg2monolem1  25705  musum  27155  lgsquadlem2  27346  umgr2v2evd2  29550  frgrregorufr0  30348  ubthlem1  30894  xrsclat  33042  psgndmfi  33129  primefldgen1  33352  zarcls0  33974  ordtrest2NEWlem  34028  hasheuni  34191  measvuni  34320  imambfm  34368  subfacp1lem6  35328  connpconn  35378  cvmliftmolem2  35425  cvmlift2lem12  35457  poimirlem28  37788  fdc  37885  isbnd3  37924  pmap1N  39966  pol1N  40109  dia1N  41252  dihwN  41488  vdioph  42963  fiphp3d  43003  stirlinglem14  46273  fvmptrabdm  47481  suppdm  48698