Theorem spc2gv 3543

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

Hypothesis

Ref	Expression
spc2egv.1	⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spc2gv	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜓,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem spc2gv

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  rspc2gv  3575  trel  5201  elovmpo  7606  seqf1olem2  13998  seqf1o  13999  fi1uzind  14463  brfi1indALT  14466  pslem  18532  cnmpt12  23645  cnmpt22  23652  mclsppslem  35784  mbfresfi  38004  lpolconN  41950  ismrcd2  43148  ismrc  43150  euendfunc  50016