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

Theorem rabbia2 3439
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 3438 . 2 (⊤ → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
43mptru 1547 1 {𝑥𝐴𝜓} = {𝑥𝐵𝜒}
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wtru 1541  wcel 2108  {crab 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437
This theorem is referenced by:  rabbiia  3440  rabswap  3446  rabeqi  3450  rabrabi  3456  f1ossf1o  7148  finsumvtxdg2ssteplem3  29565  clwlknf1oclwwlkn  30103  clwwlknon2x  30122  numclwwlkovh  30392  ballotlem2  34491  smflim  46792  smflim2  46821  smflimsuplem1  46835  smflimsup  46843  sprvalpwn0  47470
  Copyright terms: Public domain W3C validator