Metamath Proof Explorer


Theorem abbii

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

Ref Expression
Hypothesis abbii.1 φψ
Assertion abbii x|φ=x|ψ

Proof

Step Hyp Ref Expression
1 abbii.1 φψ
2 abbi xφψx|φ=x|ψ
3 2 1 mpg x|φ=x|ψ