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

Theorem rabbii 3420
Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3427. (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 3419 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2111  {crab 3110
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-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rab 3115
This theorem is referenced by:  dfdif3  4042  elneldisj  4296  elnelun  4297  dfepfr  5504  epfrc  5505  fndmdifcom  6790  fniniseg2  6809  uniordint  7501  dfoi  8959  kmlem3  9563  alephsuc3  9991  hashbclem  13806  gcdcom  15852  gcdass  15885  lcmcom  15927  lcmass  15948  acsfn0  16923  dfrhm2  19465  lbsextg  19927  dmtopon  21528  fctop2  21610  ordtrest2  21809  qtopres  22303  tsmsfbas  22733  shftmbl  24142  ppiub  25788  rpvmasum  26110  umgrislfupgrlem  26915  finsumvtxdg2ssteplem1  27335  clwwlknclwwlkdifnum  27765  clwwlknon2num  27890  dlwwlknondlwlknonf1o  28150  numclwlk1lem1  28154  aciunf1  30426  fpwrelmapffslem  30494  ordtrest2NEW  31276  unelldsys  31527  rossros  31549  aean  31613  orvcval2  31826  subfacp1lem6  32542  satfv1  32720  noextendlt  33286  nosepne  33295  nosepdm  33298  nosupbnd2lem1  33325  noetalem3  33329  itg2addnclem2  35106  scottexf  35603  scott0f  35604  rabbieq  35669  refsymrels2  35958  dfeqvrels2  35980  refrelsredund3  36026  dffunsALTV5  36077  glbconxN  36671  3anrabdioph  39718  3orrabdioph  39719  rexrabdioph  39730  2rexfrabdioph  39732  3rexfrabdioph  39733  4rexfrabdioph  39734  6rexfrabdioph  39735  7rexfrabdioph  39736  elnn0rabdioph  39739  elnnrabdioph  39743  rabren3dioph  39751  rmydioph  39950  rmxdioph  39952  expdiophlem2  39958  relintab  40278  sqrtcvallem1  40326  uzmptshftfval  41045  binomcxplemdvsum  41054  binomcxp  41056  dvnprod  42586  ovnsubadd  43206  hoidmv1lelem3  43227  hoidmvlelem3  43231  ovolval3  43281  ovolval4lem2  43284  ovolval5lem3  43288  smflimlem4  43402
  Copyright terms: Public domain W3C validator