Theorem rabid2 3444

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∀wral 3076  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413

This theorem is used by:  iinrab2  5028  riinrab  5044  dmmptg  6238  frpoinsg  6341  dmmptd  6678  fneqeql  7039  fmpt  7104  tfisg  7851  zfrep6OLD  7953  frinsg  9736  axdc2lem  10453  ioomax  13478  iccmax  13479  hashbc  14521  lcmf0  16727  dfphi2  16868  phiprmpw  16870  phisum  16885  isnsg4  19293  symggen2  19601  psgnfvalfi  19643  lssuni  21126  psgnghm2  21797  ocv0  21893  dsmmfi  21954  frlmfibas  21978  frlmlbs  22013  psr1baslem  22413  ordtrest2lem  23431  comppfsc  23761  xkouni  23828  xkoccn  23848  tsmsfbas  24357  clsocv  25481  ehlbase  25646  ovolicc2lem4  25751  itg2monolem1  25981  musum  27430  lgsquadlem2  27620  umgr2v2evd2  29990  frgrregorufr0  30807  ubthlem1  31354  xrsclat  33454  psgndmfi  33541  primefldgen1  33765  zarcls0  34381  ordtrest2NEWlem  34435  hasheuni  34598  measvuni  34728  imambfm  34776  subfacp1lem6  35767  connpconn  35817  cvmliftmolem2  35864  cvmlift2lem12  35896  poimirlem28  38400  fdc  38498  isbnd3  38537  pmap1N  40643  pol1N  40786  dia1N  41929  dihwN  42165  vdioph  43627  fiphp3d  43663  stirlinglem14  46918  fvmptrabdm  48184  suppdm  49443