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

Theorem spc2gv 3599
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 3598 . . 3 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ∃𝑥𝑦 ¬ 𝜑))
4 2nalexn 1827 . . 3 (¬ ∀𝑥𝑦𝜑 ↔ ∃𝑥𝑦 ¬ 𝜑)
53, 4imbitrrdi 252 . 2 ((𝐴𝑉𝐵𝑊) → (¬ 𝜓 → ¬ ∀𝑥𝑦𝜑))
65con4d 115 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1537   = wceq 1539  wex 1778  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-clel 2815
This theorem is referenced by:  rspc2gv  3631  trel  5267  elovmpo  7679  seqf1olem2  14084  seqf1o  14085  fi1uzind  14547  brfi1indALT  14550  pslem  18618  cnmpt12  23676  cnmpt22  23683  mclsppslem  35589  mbfresfi  37674  lpolconN  41490  ismrcd2  42715  ismrc  42717  euendfunc  49184
  Copyright terms: Public domain W3C validator