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 (A = B \leftrightarrow \exists x (x = A \land x = B))$

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

Metamath Proof Explorer