Theorem rabid2 3454

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∀wral 3052  {crab 3420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rab 3421

This theorem is referenced by:  iinrab2  5051  riinrab  5065  dmmptg  6236  frpoinsg  6337  wfisgOLD  6348  dmmptd  6688  fneqeql  7041  fmpt  7105  tfisg  7854  zfrep6  7958  frinsg  9770  axdc2lem  10467  ioomax  13444  iccmax  13445  hashbc  14476  lcmf0  16658  dfphi2  16798  phiprmpw  16800  phisum  16815  isnsg4  19155  symggen2  19457  psgnfvalfi  19499  lssuni  20901  psgnghm2  21546  ocv0  21642  dsmmfi  21703  frlmfibas  21727  frlmlbs  21762  psr1baslem  22125  ordtrest2lem  23146  comppfsc  23475  xkouni  23542  xkoccn  23562  tsmsfbas  24071  clsocv  25207  ehlbase  25372  ovolicc2lem4  25478  itg2monolem1  25708  musum  27158  lgsquadlem2  27349  umgr2v2evd2  29512  frgrregorufr0  30310  ubthlem1  30856  xrsclat  33008  psgndmfi  33114  primefldgen1  33320  zarcls0  33904  ordtrest2NEWlem  33958  hasheuni  34121  measvuni  34250  imambfm  34299  subfacp1lem6  35212  connpconn  35262  cvmliftmolem2  35309  cvmlift2lem12  35341  poimirlem28  37677  fdc  37774  isbnd3  37813  pmap1N  39791  pol1N  39934  dia1N  41077  dihwN  41313  vdioph  42777  fiphp3d  42817  stirlinglem14  46096  fvmptrabdm  47302  suppdm  48466