Metamath Proof Explorer


Theorem rabbia2

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis rabbia2.1 ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) )
Assertion rabbia2 { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 }

Proof

Step Hyp Ref Expression
1 rabbia2.1 ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) )
2 1 a1i ( ⊤ → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) ) )
3 2 rabbidva2 ( ⊤ → { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 } )
4 3 mptru { 𝑥𝐴𝜓 } = { 𝑥𝐵𝜒 }