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

Theorem rabbia2 3433
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 3432 . 2 (⊤ → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
43mptru 1546 1 {𝑥𝐴𝜓} = {𝑥𝐵𝜒}
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1539  wtru 1540  wcel 2104  {crab 3430
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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-rab 3431
This theorem is referenced by:  rabbiia  3434  rabswap  3439  rabeqi  3443  rabrabi  3448  f1ossf1o  7127  finsumvtxdg2ssteplem3  29071  clwlknf1oclwwlkn  29604  clwwlknon2x  29623  numclwwlkovh  29893  ballotlem2  33785  smflim  45791  smflim2  45820  smflimsuplem1  45834  smflimsup  45842  sprvalpwn0  46449
  Copyright terms: Public domain W3C validator