This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∀ 𝑦 𝜓 → 𝜒 ) )