Theorem rabid2 3469

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

Syntax hints:   ↔ wb 206   = wceq 1539  ∀wral 3060  {crab 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rab 3436

This theorem is referenced by:  iinrab2  5069  riinrab  5083  dmmptg  6261  frpoinsg  6363  wfisgOLD  6374  dmmptd  6712  fneqeql  7065  fmpt  7129  tfisg  7876  zfrep6  7980  frinsg  9792  axdc2lem  10489  ioomax  13463  iccmax  13464  hashbc  14493  lcmf0  16672  dfphi2  16812  phiprmpw  16814  phisum  16829  isnsg4  19186  symggen2  19490  psgnfvalfi  19532  lssuni  20938  psgnghm2  21600  ocv0  21696  dsmmfi  21759  frlmfibas  21783  frlmlbs  21818  psr1baslem  22187  ordtrest2lem  23212  comppfsc  23541  xkouni  23608  xkoccn  23628  tsmsfbas  24137  clsocv  25285  ehlbase  25450  ovolicc2lem4  25556  itg2monolem1  25786  musum  27235  lgsquadlem2  27426  umgr2v2evd2  29546  frgrregorufr0  30344  ubthlem1  30890  xrsclat  33014  psgndmfi  33119  primefldgen1  33324  zarcls0  33868  ordtrest2NEWlem  33922  hasheuni  34087  measvuni  34216  imambfm  34265  subfacp1lem6  35191  connpconn  35241  cvmliftmolem2  35288  cvmlift2lem12  35320  poimirlem28  37656  fdc  37753  isbnd3  37792  pmap1N  39770  pol1N  39913  dia1N  41056  dihwN  41292  vdioph  42795  fiphp3d  42835  stirlinglem14  46107  fvmptrabdm  47310  suppdm  48432