MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spc2gv Structured version   Visualization version   GIF version

Theorem spc2gv 3561
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
StepHypRef Expression
1 spc2egv.1 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
21notbid 318 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (¬ 𝜑 ↔ ¬ 𝜓))
32spc2egv 3560 . . 3 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ∃𝑥𝑦 ¬ 𝜑))
4 2nalexn 1831 . . 3 (¬ ∀𝑥𝑦𝜑 ↔ ∃𝑥𝑦 ¬ 𝜑)
53, 4syl6ibr 252 . 2 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ¬ ∀𝑥𝑦𝜑))
65con4d 115 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811
This theorem is referenced by:  rspc2gv  3591  trel  5235  elovmpo  7602  seqf1olem2  13957  seqf1o  13958  fi1uzind  14405  brfi1indALT  14408  pslem  18469  cnmpt12  23041  cnmpt22  23048  mclsppslem  34241  mbfresfi  36174  lpolconN  40000  ismrcd2  41069  ismrc  41071
  Copyright terms: Public domain W3C validator