rspc2

Description: Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012)

	Ref	Expression
Hypotheses	rspc2.1	$⊢ Ⅎ x χ$
	rspc2.2	$⊢ Ⅎ y ψ$
	rspc2.3	$⊢ x = A \to (φ \leftrightarrow χ)$
	rspc2.4	$⊢ y = B \to (χ \leftrightarrow ψ)$
Assertion	rspc2	$⊢ (A \in C \land B \in D) \to (\forall x \in C \forall y \in D φ \to ψ)$

Step	Hyp	Ref	Expression
1		rspc2.1	$⊢ Ⅎ x χ$
2		rspc2.2	$⊢ Ⅎ y ψ$
3		rspc2.3	$⊢ x = A \to (φ \leftrightarrow χ)$
4		rspc2.4	$⊢ y = B \to (χ \leftrightarrow ψ)$
5		nfcv	$⊢ \underline{Ⅎ} x D$
6	5 1	nfralw	$⊢ Ⅎ x \forall y \in D χ$
7	3	ralbidv	$⊢ x = A \to (\forall y \in D φ \leftrightarrow \forall y \in D χ)$
8	6 7	rspc	$⊢ A \in C \to (\forall x \in C \forall y \in D φ \to \forall y \in D χ)$
9	2 4	rspc	$⊢ B \in D \to (\forall y \in D χ \to ψ)$
10	8 9	sylan9	$⊢ (A \in C \land B \in D) \to (\forall x \in C \forall y \in D φ \to ψ)$

Metamath Proof Explorer