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 { 𝑥𝜑 } = 𝐴
Assertion eqabcri ( 𝜑𝑥𝐴 )

Proof

Step Hyp Ref Expression
1 eqabcri.1 { 𝑥𝜑 } = 𝐴
2 1 eqcomi 𝐴 = { 𝑥𝜑 }
3 2 eqabri ( 𝑥𝐴𝜑 )
4 3 bicomi ( 𝜑𝑥𝐴 )