Metamath Proof Explorer


Theorem abbi2i

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993) Avoid ax-11 . (Revised by Wolf Lammen, 6-May-2023)

Ref Expression
Hypothesis abbi2i.1 x A φ
Assertion abbi2i A = x | φ

Proof

Step Hyp Ref Expression
1 abbi2i.1 x A φ
2 1 a1i x A φ
3 2 abbi2dv A = x | φ
4 3 mptru A = x | φ