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

Theorem spc2gv 3269
 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 307 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (¬ 𝜑 ↔ ¬ 𝜓))
32spc2egv 3268 . . 3 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ∃𝑥𝑦 ¬ 𝜑))
4 2nalexn 1745 . . 3 (¬ ∀𝑥𝑦𝜑 ↔ ∃𝑥𝑦 ¬ 𝜑)
53, 4syl6ibr 241 . 2 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ¬ ∀𝑥𝑦𝜑))
65con4d 113 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑦𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175 This theorem is referenced by:  trel  4687  elovmpt2  6777  seqf1olem2  12703  seqf1o  12704  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  pslem  17029  cnmpt12  21280  cnmpt22  21287  frg2woteqm  26586  mclsppslem  30734  mbfresfi  32626  lpolconN  35794  ismrcd2  36280  ismrc  36282
 Copyright terms: Public domain W3C validator