Metamath Proof Explorer


Theorem abeq1i

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

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

Proof

Step Hyp Ref Expression
1 abeq1i.1
 |-  { x | ph } = A
2 1 eqcomi
 |-  A = { x | ph }
3 2 abeq2i
 |-  ( x e. A <-> ph )
4 3 bicomi
 |-  ( ph <-> x e. A )