Theorem eqvincg

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

	Ref	Expression
Assertion	eqvincg	|- ( A e. V -> ( A = B <-> E. x ( x = A /\ x = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		elisset	|- ( A e. V -> E. x x = A )
2		ax-1	|- ( x = A -> ( A = B -> x = A ) )
3		eqtr	|- ( ( x = A /\ A = B ) -> x = B )
4	3	ex	|- ( x = A -> ( A = B -> x = B ) )
5	2 4	jca	|- ( x = A -> ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) )
6	5	eximi	|- ( E. x x = A -> E. x ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) )
7		pm3.43	|- ( ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) -> ( A = B -> ( x = A /\ x = B ) ) )
8	7	eximi	|- ( E. x ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) -> E. x ( A = B -> ( x = A /\ x = B ) ) )
9	1 6 8	3syl	|- ( A e. V -> E. x ( A = B -> ( x = A /\ x = B ) ) )
10		19.37v	|- ( E. x ( A = B -> ( x = A /\ x = B ) ) <-> ( A = B -> E. x ( x = A /\ x = B ) ) )
11	9 10	sylib	|- ( A e. V -> ( A = B -> E. x ( x = A /\ x = B ) ) )
12		eqtr2	|- ( ( x = A /\ x = B ) -> A = B )
13	12	exlimiv	|- ( E. x ( x = A /\ x = B ) -> A = B )
14	11 13	impbid1	|- ( A e. V -> ( A = B <-> E. x ( x = A /\ x = B ) ) )