spc2ed

Description: Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017)

	Ref	Expression
Hypotheses	spc2ed.x	$⊢ Ⅎ x χ$
	spc2ed.y	$⊢ Ⅎ y χ$
	spc2ed.1	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	spc2ed	$⊢ (φ \land (A \in V \land B \in W)) \to (χ \to \exists x \exists y ψ)$

Proof

Step	Hyp	Ref	Expression
1		spc2ed.x	$⊢ Ⅎ x χ$
2		spc2ed.y	$⊢ Ⅎ y χ$
3		spc2ed.1	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
4		elisset	$⊢ A \in V \to \exists x x = A$
5		elisset	$⊢ B \in W \to \exists y y = B$
6	4 5	anim12i	$⊢ (A \in V \land B \in W) \to (\exists x x = A \land \exists y y = B)$
7		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
8	6 7	sylibr	$⊢ (A \in V \land B \in W) \to \exists x \exists y (x = A \land y = B)$
9		nfv	$⊢ Ⅎ x φ$
10	9 1	nfan	$⊢ Ⅎ x (φ \land χ)$
11		nfv	$⊢ Ⅎ y φ$
12	11 2	nfan	$⊢ Ⅎ y (φ \land χ)$
13		anass	$⊢ ((χ \land φ) \land (x = A \land y = B)) \leftrightarrow (χ \land (φ \land (x = A \land y = B)))$
14		ancom	$⊢ (χ \land φ) \leftrightarrow (φ \land χ)$
15	14	anbi1i	$⊢ ((χ \land φ) \land (x = A \land y = B)) \leftrightarrow ((φ \land χ) \land (x = A \land y = B))$
16	13 15	bitr3i	$⊢ (χ \land (φ \land (x = A \land y = B))) \leftrightarrow ((φ \land χ) \land (x = A \land y = B))$
17	3	biimparc	$⊢ (χ \land (φ \land (x = A \land y = B))) \to ψ$
18	16 17	sylbir	$⊢ ((φ \land χ) \land (x = A \land y = B)) \to ψ$
19	18	ex	$⊢ (φ \land χ) \to ((x = A \land y = B) \to ψ)$
20	12 19	eximd	$⊢ (φ \land χ) \to (\exists y (x = A \land y = B) \to \exists y ψ)$
21	10 20	eximd	$⊢ (φ \land χ) \to (\exists x \exists y (x = A \land y = B) \to \exists x \exists y ψ)$
22	21	impancom	$⊢ (φ \land \exists x \exists y (x = A \land y = B)) \to (χ \to \exists x \exists y ψ)$
23	8 22	sylan2	$⊢ (φ \land (A \in V \land B \in W)) \to (χ \to \exists x \exists y ψ)$

Metamath Proof Explorer

Theorem spc2ed

Proof