Metamath Proof Explorer


Theorem eqabri

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996) (Proof shortened by Wolf Lammen, 15-Nov-2019)

Ref Expression
Hypothesis eqabri.1
|- A = { x | ph }
Assertion eqabri
|- ( x e. A <-> ph )

Proof

Step Hyp Ref Expression
1 eqabri.1
 |-  A = { x | ph }
2 1 a1i
 |-  ( T. -> A = { x | ph } )
3 2 eqabrd
 |-  ( T. -> ( x e. A <-> ph ) )
4 3 mptru
 |-  ( x e. A <-> ph )