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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	abeq2f	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abeq2f.0	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
3	1 2	cleqf	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)$$
4		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
5	4	bibi2i	$$⊢\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)\leftrightarrow \left(x\in A\leftrightarrow \phi \right)$$
6	5	albii	$$⊢\forall x\left(x\in A\leftrightarrow x\in \left\{x|\phi \right\}\right)\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$
7	3 6	bitri	$$⊢A=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \phi \right)$$