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

Theorem spc2egv 3598
Description: Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
Hypothesis
Ref Expression
spc2egv.1 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
Assertion
Ref Expression
spc2egv ((𝐴𝑉𝐵𝑊) → (𝜓 → ∃𝑥𝑦𝜑))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem spc2egv
StepHypRef Expression
1 elisset 2820 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 elisset 2820 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
31, 2anim12i 613 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4 exdistrv 1952 . . 3 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
53, 4sylibr 234 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵))
6 spc2egv.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
76biimprcd 250 . . 3 (𝜓 → ((𝑥 = 𝐴𝑦 = 𝐵) → 𝜑))
872eximdv 1916 . 2 (𝜓 → (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → ∃𝑥𝑦𝜑))
95, 8syl5com 31 1 ((𝐴𝑉𝐵𝑊) → (𝜓 → ∃𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wex 1775  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-clel 2813
This theorem is referenced by:  spc2gv  3599  spc3egv  3602  spc2ev  3606  tpres  7220  addsrpr  11112  mulsrpr  11113  2pthon3v  29972  umgr2wlk  29978  0pthonv  30157  1pthon2v  30181  satfv1  35347  sat1el2xp  35363  dvnprodlem1  45901  dfatcolem  47204  fundcmpsurbijinj  47334
  Copyright terms: Public domain W3C validator