Metamath Proof Explorer


Theorem abeq2f

Description: Equality of a class variable and a class abstraction. In this version, the fact that x is a nonfree variable in A is explicitly stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017) Avoid ax-13 . (Revised by Wolf Lammen, 13-May-2023)

Ref Expression
Hypothesis abeq2f.0 _xA
Assertion abeq2f A=x|φxxAφ

Proof

Step Hyp Ref Expression
1 abeq2f.0 _xA
2 nfab1 _xx|φ
3 1 2 cleqf A=x|φxxAxx|φ
4 abid xx|φφ
5 4 bibi2i xAxx|φxAφ
6 5 albii xxAxx|φxxAφ
7 3 6 bitri A=x|φxxAφ