Theorem eqvincf

Description: A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003)

	Ref	Expression
Hypotheses	eqvincf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	eqvincf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	eqvincf.3	$$⊢A\in \mathrm{V}$$
Assertion	eqvincf	$$⊢A=B\leftrightarrow \exists x\left(x=A\wedge x=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqvincf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		eqvincf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		eqvincf.3	$$⊢A\in \mathrm{V}$$
4	3	eqvinc	$$⊢A=B\leftrightarrow \exists y\left(y=A\wedge y=B\right)$$
5	1	nfeq2	$$⊢Ⅎxy=A$$
6	2	nfeq2	$$⊢Ⅎxy=B$$
7	5 6	nfan	$$⊢Ⅎx\left(y=A\wedge y=B\right)$$
8		nfv	$$⊢Ⅎy\left(x=A\wedge x=B\right)$$
9		eqeq1	$$⊢y=x\to \left(y=A\leftrightarrow x=A\right)$$
10		eqeq1	$$⊢y=x\to \left(y=B\leftrightarrow x=B\right)$$
11	9 10	anbi12d	$$⊢y=x\to \left(\left(y=A\wedge y=B\right)\leftrightarrow \left(x=A\wedge x=B\right)\right)$$
12	7 8 11	cbvexv1	$$⊢\exists y\left(y=A\wedge y=B\right)\leftrightarrow \exists x\left(x=A\wedge x=B\right)$$
13	4 12	bitri	$$⊢A=B\leftrightarrow \exists x\left(x=A\wedge x=B\right)$$