Metamath Proof Explorer


Theorem eqabi

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 eqabi.1 x A φ
Assertion eqabi A = x | φ

Proof

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