Theorem rabid2 3442

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∀wral 3045  {crab 3408

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rab 3409

This theorem is referenced by:  iinrab2  5036  riinrab  5050  dmmptg  6217  frpoinsg  6318  dmmptd  6665  fneqeql  7020  fmpt  7084  tfisg  7832  zfrep6  7935  frinsg  9710  axdc2lem  10407  ioomax  13389  iccmax  13390  hashbc  14424  lcmf0  16610  dfphi2  16750  phiprmpw  16752  phisum  16767  isnsg4  19105  symggen2  19407  psgnfvalfi  19449  lssuni  20851  psgnghm2  21496  ocv0  21592  dsmmfi  21653  frlmfibas  21677  frlmlbs  21712  psr1baslem  22075  ordtrest2lem  23096  comppfsc  23425  xkouni  23492  xkoccn  23512  tsmsfbas  24021  clsocv  25156  ehlbase  25321  ovolicc2lem4  25427  itg2monolem1  25657  musum  27107  lgsquadlem2  27298  umgr2v2evd2  29461  frgrregorufr0  30259  ubthlem1  30805  xrsclat  32955  psgndmfi  33061  primefldgen1  33277  zarcls0  33864  ordtrest2NEWlem  33918  hasheuni  34081  measvuni  34210  imambfm  34259  subfacp1lem6  35172  connpconn  35222  cvmliftmolem2  35269  cvmlift2lem12  35301  poimirlem28  37637  fdc  37734  isbnd3  37773  pmap1N  39756  pol1N  39899  dia1N  41042  dihwN  41278  vdioph  42760  fiphp3d  42800  stirlinglem14  46078  fvmptrabdm  47284  suppdm  48489