Theorem spc2gv

Description: Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004)

	Ref	Expression
Hypothesis	spc2egv.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spc2gv	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\forall y\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spc2egv.1	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
2	1	notbid	$$⊢\left(x=A\wedge y=B\right)\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	2	spc2egv	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg \psi \to \exists x\exists y\neg \phi \right)$$
4		2nalexn	$$⊢\neg \forall x\forall y\phi \leftrightarrow \exists x\exists y\neg \phi$$
5	3 4	imbitrrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg \psi \to \neg \forall x\forall y\phi \right)$$
6	5	con4d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\forall y\phi \to \psi \right)$$