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

Theorem spc2gv 3600
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 319 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (¬ 𝜑 ↔ ¬ 𝜓))
32spc2egv 3599 . . 3 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ∃𝑥𝑦 ¬ 𝜑))
4 2nalexn 1819 . . 3 (¬ ∀𝑥𝑦𝜑 ↔ ∃𝑥𝑦 ¬ 𝜑)
53, 4syl6ibr 253 . 2 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ¬ ∀𝑥𝑦𝜑))
65con4d 115 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wex 1771  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  rspc2gv  3631  trel  5171  elovmpo  7379  seqf1olem2  13400  seqf1o  13401  fi1uzind  13845  brfi1indALT  13848  pslem  17806  cnmpt12  22205  cnmpt22  22212  mclsppslem  32728  mbfresfi  34820  lpolconN  38505  ismrcd2  39176  ismrc  39178
  Copyright terms: Public domain W3C validator