Theorem rabid2 3424

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

Syntax hints:   ↔ wb 207   = wceq 1547  ∀wral 3053  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rab 3392

This theorem is referenced by:  iinrab2  5000  riinrab  5014  dmmptg  6194  frpoinsg  6295  dmmptd  6631  fneqeql  6988  fmpt  7052  tfisg  7795  zfrep6OLD  7898  frinsg  9667  axdc2lem  10362  ioomax  13367  iccmax  13368  hashbc  14407  lcmf0  16595  dfphi2  16736  phiprmpw  16738  phisum  16753  isnsg4  19134  symggen2  19438  psgnfvalfi  19480  lssuni  20930  psgnghm2  21557  ocv0  21653  dsmmfi  21714  frlmfibas  21738  frlmlbs  21773  psr1baslem  22171  ordtrest2lem  23187  comppfsc  23516  xkouni  23583  xkoccn  23603  tsmsfbas  24112  clsocv  25236  ehlbase  25401  ovolicc2lem4  25506  itg2monolem1  25736  musum  27173  lgsquadlem2  27363  umgr2v2evd2  29615  frgrregorufr0  30413  ubthlem1  30960  xrsclat  33091  psgndmfi  33180  primefldgen1  33406  zarcls0  34061  ordtrest2NEWlem  34115  hasheuni  34278  measvuni  34407  imambfm  34455  subfacp1lem6  35422  connpconn  35472  cvmliftmolem2  35519  cvmlift2lem12  35551  poimirlem28  38024  fdc  38121  isbnd3  38160  pmap1N  40268  pol1N  40411  dia1N  41554  dihwN  41790  vdioph  43237  fiphp3d  43273  stirlinglem14  46538  fvmptrabdm  47764  suppdm  49009