Metamath Proof Explorer


Theorem eqabcri

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 eqabcri.1
|- { x | ph } = A
Assertion eqabcri
|- ( ph <-> x e. A )

Proof

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