spc2d

Description: 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	spc2d	$⊢ (φ \land (A \in V \land B \in W)) \to (\forall x \forall y ψ \to χ)$

Step	Hyp	Ref	Expression
1		spc2ed.x	$⊢ Ⅎ x χ$
2		spc2ed.y	$⊢ Ⅎ y χ$
3		spc2ed.1	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
4		2nalexn	$⊢ \neg \forall x \forall y ψ \leftrightarrow \exists x \exists y \neg ψ$
5	4	con1bii	$⊢ \neg \exists x \exists y \neg ψ \leftrightarrow \forall x \forall y ψ$
6	1	nfn	$⊢ Ⅎ x \neg χ$
7	2	nfn	$⊢ Ⅎ y \neg χ$
8	3	notbid	$⊢ (φ \land (x = A \land y = B)) \to (\neg ψ \leftrightarrow \neg χ)$
9	6 7 8	spc2ed	$⊢ (φ \land (A \in V \land B \in W)) \to (\neg χ \to \exists x \exists y \neg ψ)$
10	9	con1d	$⊢ (φ \land (A \in V \land B \in W)) \to (\neg \exists x \exists y \neg ψ \to χ)$
11	5 10	biimtrrid	$⊢ (φ \land (A \in V \land B \in W)) \to (\forall x \forall y ψ \to χ)$

Metamath Proof Explorer