Theorem abeq2f

Description: Equality of a class variable and a class abstraction. In this version, the fact that x is a non-free 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	|- F/_ x A
Assertion	abeq2f	|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		abeq2f.0	|- F/_ x A
2		nfab1	|- F/_ x { x | ph }
3	1 2	cleqf	|- ( A = { x | ph } <-> A. x ( x e. A <-> x e. { x | ph } ) )
4		abid	|- ( x e. { x | ph } <-> ph )
5	4	bibi2i	|- ( ( x e. A <-> x e. { x | ph } ) <-> ( x e. A <-> ph ) )
6	5	albii	|- ( A. x ( x e. A <-> x e. { x | ph } ) <-> A. x ( x e. A <-> ph ) )
7	3 6	bitri	|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )