Theorem rabid2 3462

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

Syntax hints:   ↔ wb 205   = wceq 1539  ∀wral 3059  {crab 3430

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rab 3431

This theorem is referenced by:  class2seteq  3699  rabxm  4385  iinrab2  5072  riinrab  5086  dmmptg  6240  frpoinsg  6343  wfisgOLD  6354  dmmptd  6694  fneqeql  7046  fmpt  7110  tfisg  7845  zfrep6  7943  frinsg  9748  axdc2lem  10445  ioomax  13403  iccmax  13404  hashbc  14416  lcmf0  16575  dfphi2  16711  phiprmpw  16713  phisum  16727  isnsg4  19083  symggen2  19380  psgnfvalfi  19422  lssuni  20694  psgnghm2  21353  ocv0  21449  dsmmfi  21512  frlmfibas  21536  frlmlbs  21571  psr1baslem  21928  ordtrest2lem  22927  comppfsc  23256  xkouni  23323  xkoccn  23343  tsmsfbas  23852  clsocv  24998  ehlbase  25163  ovolicc2lem4  25269  itg2monolem1  25500  musum  26931  lgsquadlem2  27120  umgr2v2evd2  29051  frgrregorufr0  29844  ubthlem1  30390  xrsclat  32448  psgndmfi  32527  primefldgen1  32681  zarcls0  33146  ordtrest2NEWlem  33200  hasheuni  33381  measvuni  33510  imambfm  33559  subfacp1lem6  34474  connpconn  34524  cvmliftmolem2  34571  cvmlift2lem12  34603  poimirlem28  36819  fdc  36916  isbnd3  36955  pmap1N  38941  pol1N  39084  dia1N  40227  dihwN  40463  vdioph  41819  fiphp3d  41859  stirlinglem14  45101  fvmptrabdm  46299  suppdm  47278