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

Theorem rabbia2 3435
Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
rabbia2.1 ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒))
Assertion
Ref Expression
rabbia2 {𝑥𝐴𝜓} = {𝑥𝐵𝜒}

Proof of Theorem rabbia2
StepHypRef Expression
1 rabbia2.1 . . . 4 ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒))
21a1i 11 . . 3 (⊤ → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
32rabbidva2 3434 . 2 (⊤ → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
43mptru 1548 1 {𝑥𝐴𝜓} = {𝑥𝐵𝜒}
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wtru 1542  wcel 2106  {crab 3432
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-rab 3433
This theorem is referenced by:  rabbiia  3436  rabswap  3441  rabeqi  3445  rabrabi  3450  f1ossf1o  7122  finsumvtxdg2ssteplem3  28793  clwlknf1oclwwlkn  29326  clwwlknon2x  29345  numclwwlkovh  29615  ballotlem2  33475  smflim  45479  smflim2  45508  smflimsuplem1  45522  smflimsup  45530  sprvalpwn0  46137
  Copyright terms: Public domain W3C validator