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 _ x A
Assertion abeq2f A = x | φ x x A φ

Proof

Step Hyp Ref Expression
1 abeq2f.0 _ x A
2 nfab1 _ x x | φ
3 1 2 cleqf A = x | φ x x A x x | φ
4 abid x x | φ φ
5 4 bibi2i x A x x | φ x A φ
6 5 albii x x A x x | φ x x A φ
7 3 6 bitri A = x | φ x x A φ