Theorem spc2d

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

	Ref	Expression
Hypotheses	spc2ed.x	⊢ Ⅎ 𝑥 𝜒
	spc2ed.y	⊢ Ⅎ 𝑦 𝜒
	spc2ed.1	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	spc2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∀ 𝑦 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		spc2ed.x	⊢ Ⅎ 𝑥 𝜒
2		spc2ed.y	⊢ Ⅎ 𝑦 𝜒
3		spc2ed.1	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
4		2nalexn	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ¬ 𝜓 )
5	4	con1bii	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ¬ 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 𝜓 )
6	1	nfn	⊢ Ⅎ 𝑥 ¬ 𝜒
7	2	nfn	⊢ Ⅎ 𝑦 ¬ 𝜒
8	3	notbid	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
9	6 7 8	spc2ed	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ¬ 𝜒 → ∃ 𝑥 ∃ 𝑦 ¬ 𝜓 ) )
10	9	con1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ¬ ∃ 𝑥 ∃ 𝑦 ¬ 𝜓 → 𝜒 ) )
11	5 10	biimtrrid	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∀ 𝑦 𝜓 → 𝜒 ) )