MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabid2 Structured version   Visualization version   GIF version

Theorem rabid2 3337
Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
rabid2 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabid2
StepHypRef Expression
1 abeq2 2925 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
2 pm4.71 561 . . . 4 ((𝑥𝐴𝜑) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝜑)))
32albii 1821 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝜑)))
41, 3bitr4i 281 . 2 (𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ∀𝑥(𝑥𝐴𝜑))
5 df-rab 3118 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
65eqeq2i 2814 . 2 (𝐴 = {𝑥𝐴𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝜑)})
7 df-ral 3114 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
84, 6, 73bitr4i 306 1 (𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2112  {cab 2779  wral 3109  {crab 3113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-rab 3118
This theorem is referenced by:  rabxm  4297  iinrab2  4958  riinrab  4972  class2seteq  5223  dmmptg  6067  wfisg  6155  dmmptd  6469  fneqeql  6797  fmpt  6855  zfrep6  7642  axdc2lem  9863  ioomax  12804  iccmax  12805  hashbc  13811  lcmf0  15971  dfphi2  16104  phiprmpw  16106  phisum  16120  isnsg4  18314  symggen2  18594  psgnfvalfi  18636  lssuni  19707  psgnghm2  20273  ocv0  20369  dsmmfi  20430  frlmfibas  20454  frlmlbs  20489  psr1baslem  20817  ordtrest2lem  21811  comppfsc  22140  xkouni  22207  xkoccn  22227  tsmsfbas  22736  clsocv  23857  ehlbase  24022  ovolicc2lem4  24127  itg2monolem1  24357  musum  25779  lgsquadlem2  25968  umgr2v2evd2  27320  frgrregorufr0  28112  ubthlem1  28656  xrsclat  30717  psgndmfi  30793  zarcls0  31221  ordtrest2NEWlem  31273  hasheuni  31452  measvuni  31581  imambfm  31628  subfacp1lem6  32540  connpconn  32590  cvmliftmolem2  32637  cvmlift2lem12  32669  tfisg  33163  frpoinsg  33189  frinsg  33195  poimirlem28  35078  fdc  35176  isbnd3  35215  pmap1N  37056  pol1N  37199  dia1N  38342  dihwN  38578  vdioph  39707  fiphp3d  39747  dmmptdf  41841  stirlinglem14  42716  fvmptrabdm  43836  suppdm  44906
  Copyright terms: Public domain W3C validator