Theorem rabid2 3432

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∀wral 3051  {crab 3399

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 2184  ax-ext 2708

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

This theorem is referenced by:  iinrab2  5025  riinrab  5039  dmmptg  6200  frpoinsg  6301  dmmptd  6637  fneqeql  6991  fmpt  7055  tfisg  7796  zfrep6  7899  frinsg  9665  axdc2lem  10360  ioomax  13340  iccmax  13341  hashbc  14378  lcmf0  16563  dfphi2  16703  phiprmpw  16705  phisum  16720  isnsg4  19098  symggen2  19402  psgnfvalfi  19444  lssuni  20892  psgnghm2  21538  ocv0  21634  dsmmfi  21695  frlmfibas  21719  frlmlbs  21754  psr1baslem  22127  ordtrest2lem  23149  comppfsc  23478  xkouni  23545  xkoccn  23565  tsmsfbas  24074  clsocv  25208  ehlbase  25373  ovolicc2lem4  25479  itg2monolem1  25709  musum  27159  lgsquadlem2  27350  umgr2v2evd2  29603  frgrregorufr0  30401  ubthlem1  30947  xrsclat  33095  psgndmfi  33182  primefldgen1  33405  zarcls0  34027  ordtrest2NEWlem  34081  hasheuni  34244  measvuni  34373  imambfm  34421  subfacp1lem6  35381  connpconn  35431  cvmliftmolem2  35478  cvmlift2lem12  35510  poimirlem28  37851  fdc  37948  isbnd3  37987  pmap1N  40049  pol1N  40192  dia1N  41335  dihwN  41571  vdioph  43042  fiphp3d  43082  stirlinglem14  46352  fvmptrabdm  47560  suppdm  48777