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

Theorem rabbii 3289
Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3293. (Contributed by Peter Mazsa, 1-Nov-2019.)
Hypothesis
Ref Expression
rabbii.1 (𝜑𝜓)
Assertion
Ref Expression
rabbii {𝑥𝐴𝜑} = {𝑥𝐴𝜓}

Proof of Theorem rabbii
StepHypRef Expression
1 rabbii.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32rabbiia 3288 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1596  wcel 2103  {crab 3018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-rab 3023
This theorem is referenced by:  dfdif3  3828  elneldisj  4071  elnelun  4072  dfepfr  5203  epfrc  5204  fndmdifcom  6437  fniniseg2  6455  bm2.5ii  7123  dfoi  8532  kmlem3  9087  alephsuc3  9515  hashbclem  13349  gcdcom  15358  gcdass  15387  lcmcom  15429  lcmass  15450  acsfn0  16443  dfrhm2  18840  lbsextg  19285  dmtopon  20850  fctop2  20932  ordtrest2  21131  qtopres  21624  tsmsfbas  22053  shftmbl  23427  ppiub  25049  rpvmasum  25335  umgrislfupgrlem  26137  finsumvtxdg2ssteplem1  26572  clwwlknclwwlkdifnum  27022  clwwlknon2num  27174  dlwwlknondlwlknonf1o  27447  numclwlk1lem1  27451  aciunf1  29693  fpwrelmapffslem  29737  ordtrest2NEW  30199  unelldsys  30451  rossros  30473  aean  30537  orvcval2  30750  subfacp1lem6  31395  noextendlt  32049  nosepne  32058  nosepdm  32061  nosupbnd2lem1  32088  noetalem3  32092  itg2addnclem2  33694  scottexf  34208  scott0f  34209  rabbieq  34258  refsymrels2  34551  glbconxN  35084  3anrabdioph  37765  3orrabdioph  37766  rexrabdioph  37777  2rexfrabdioph  37779  3rexfrabdioph  37780  4rexfrabdioph  37781  6rexfrabdioph  37782  7rexfrabdioph  37783  elnn0rabdioph  37786  elnnrabdioph  37790  rabren3dioph  37798  rmydioph  38000  rmxdioph  38002  expdiophlem2  38008  relintab  38308  uzmptshftfval  38964  binomcxplemdvsum  38973  binomcxp  38975  dvnprod  40584  ovnsubadd  41209  hoidmv1lelem3  41230  hoidmvlelem3  41234  ovolval3  41284  ovolval4lem2  41287  ovolval5lem3  41291  smflimlem4  41405
  Copyright terms: Public domain W3C validator