Theorem rabid2 3422

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∀wral 3051  {crab 3389

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rab 3390

This theorem is referenced by:  iinrab2  5012  riinrab  5026  dmmptg  6206  frpoinsg  6307  dmmptd  6643  fneqeql  6998  fmpt  7062  tfisg  7805  zfrep6OLD  7908  frinsg  9675  axdc2lem  10370  ioomax  13375  iccmax  13376  hashbc  14415  lcmf0  16603  dfphi2  16744  phiprmpw  16746  phisum  16761  isnsg4  19142  symggen2  19446  psgnfvalfi  19488  lssuni  20934  psgnghm2  21561  ocv0  21657  dsmmfi  21718  frlmfibas  21742  frlmlbs  21777  psr1baslem  22148  ordtrest2lem  23168  comppfsc  23497  xkouni  23564  xkoccn  23584  tsmsfbas  24093  clsocv  25217  ehlbase  25382  ovolicc2lem4  25487  itg2monolem1  25717  musum  27154  lgsquadlem2  27344  umgr2v2evd2  29596  frgrregorufr0  30394  ubthlem1  30941  xrsclat  33071  psgndmfi  33159  primefldgen1  33382  zarcls0  34012  ordtrest2NEWlem  34066  hasheuni  34229  measvuni  34358  imambfm  34406  subfacp1lem6  35367  connpconn  35417  cvmliftmolem2  35464  cvmlift2lem12  35496  poimirlem28  37969  fdc  38066  isbnd3  38105  pmap1N  40213  pol1N  40356  dia1N  41499  dihwN  41735  vdioph  43211  fiphp3d  43247  stirlinglem14  46515  fvmptrabdm  47741  suppdm  48986