Theorem eqvincg

Description: A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017)

	Ref	Expression
Assertion	eqvincg	$$⊢A\in V\to \left(A=B\leftrightarrow \exists x\left(x=A\wedge x=B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elisset	$$⊢A\in V\to \exists xx=A$$
2		ax-1	$$⊢x=A\to \left(A=B\to x=A\right)$$
3		eqtr	$$⊢\left(x=A\wedge A=B\right)\to x=B$$
4	3	ex	$$⊢x=A\to \left(A=B\to x=B\right)$$
5	2 4	jca	$$⊢x=A\to \left(\left(A=B\to x=A\right)\wedge \left(A=B\to x=B\right)\right)$$
6	5	eximi	$$⊢\exists xx=A\to \exists x\left(\left(A=B\to x=A\right)\wedge \left(A=B\to x=B\right)\right)$$
7		pm3.43	$$⊢\left(\left(A=B\to x=A\right)\wedge \left(A=B\to x=B\right)\right)\to \left(A=B\to \left(x=A\wedge x=B\right)\right)$$
8	7	eximi	$$⊢\exists x\left(\left(A=B\to x=A\right)\wedge \left(A=B\to x=B\right)\right)\to \exists x\left(A=B\to \left(x=A\wedge x=B\right)\right)$$
9	1 6 8	3syl	$$⊢A\in V\to \exists x\left(A=B\to \left(x=A\wedge x=B\right)\right)$$
10		19.37v	$$⊢\exists x\left(A=B\to \left(x=A\wedge x=B\right)\right)\leftrightarrow \left(A=B\to \exists x\left(x=A\wedge x=B\right)\right)$$
11	9 10	sylib	$$⊢A\in V\to \left(A=B\to \exists x\left(x=A\wedge x=B\right)\right)$$
12		eqtr2	$$⊢\left(x=A\wedge x=B\right)\to A=B$$
13	12	exlimiv	$$⊢\exists x\left(x=A\wedge x=B\right)\to A=B$$
14	11 13	impbid1	$$⊢A\in V\to \left(A=B\leftrightarrow \exists x\left(x=A\wedge x=B\right)\right)$$