Theorem spc2gv

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

	Ref	Expression
Hypothesis	spc2egv.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	spc2gv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∀ 𝑦 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		spc2egv.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
2	1	notbid	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3	2	spc2egv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝜓 → ∃ 𝑥 ∃ 𝑦 ¬ 𝜑 ) )
4		2nalexn	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ¬ 𝜑 )
5	3 4	imbitrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝜓 → ¬ ∀ 𝑥 ∀ 𝑦 𝜑 ) )
6	5	con4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∀ 𝑦 𝜑 → 𝜓 ) )