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

Theorem spc2gv 3590
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 317 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (¬ 𝜑 ↔ ¬ 𝜓))
32spc2egv 3589 . . 3 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ∃𝑥𝑦 ¬ 𝜑))
4 2nalexn 1830 . . 3 (¬ ∀𝑥𝑦𝜑 ↔ ∃𝑥𝑦 ¬ 𝜑)
53, 4syl6ibr 251 . 2 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ¬ ∀𝑥𝑦𝜑))
65con4d 115 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1539   = wceq 1541  wex 1781  wcel 2106
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 1913  ax-6 1971  ax-7 2011  ax-8 2108
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-clel 2810
This theorem is referenced by:  rspc2gv  3621  trel  5274  elovmpo  7650  seqf1olem2  14007  seqf1o  14008  fi1uzind  14457  brfi1indALT  14460  pslem  18524  cnmpt12  23170  cnmpt22  23177  mclsppslem  34569  mbfresfi  36529  lpolconN  40353  ismrcd2  41427  ismrc  41429
  Copyright terms: Public domain W3C validator