Theorem rabid2 3451

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

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

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rab 3419

This theorem is used by:  iinrab2  5036  riinrab  5052  dmmptg  6245  frpoinsg  6348  dmmptd  6684  fneqeql  7045  fmpt  7109  tfisg  7856  zfrep6OLD  7958  frinsg  9730  axdc2lem  10447  ioomax  13467  iccmax  13468  hashbc  14510  lcmf0  16716  dfphi2  16857  phiprmpw  16859  phisum  16874  isnsg4  19279  symggen2  19587  psgnfvalfi  19629  lssuni  21112  psgnghm2  21783  ocv0  21879  dsmmfi  21940  frlmfibas  21964  frlmlbs  21999  psr1baslem  22397  ordtrest2lem  23412  comppfsc  23742  xkouni  23809  xkoccn  23829  tsmsfbas  24338  clsocv  25462  ehlbase  25627  ovolicc2lem4  25732  itg2monolem1  25962  musum  27408  lgsquadlem2  27598  umgr2v2evd2  29937  frgrregorufr0  30748  ubthlem1  31295  xrsclat  33397  psgndmfi  33484  primefldgen1  33708  zarcls0  34324  ordtrest2NEWlem  34378  hasheuni  34541  measvuni  34671  imambfm  34719  subfacp1lem6  35716  connpconn  35766  cvmliftmolem2  35813  cvmlift2lem12  35845  poimirlem28  38358  fdc  38456  isbnd3  38495  pmap1N  40601  pol1N  40744  dia1N  41887  dihwN  42123  vdioph  43570  fiphp3d  43606  stirlinglem14  46861  fvmptrabdm  48090  suppdm  49349