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

Theorem spc2egv 3599
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 2823 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 elisset 2823 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
31, 2anim12i 613 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4 exdistrv 1955 . . 3 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
53, 4sylibr 234 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵))
6 spc2egv.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
76biimprcd 250 . . 3 (𝜓 → ((𝑥 = 𝐴𝑦 = 𝐵) → 𝜑))
872eximdv 1919 . 2 (𝜓 → (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → ∃𝑥𝑦𝜑))
95, 8syl5com 31 1 ((𝐴𝑉𝐵𝑊) → (𝜓 → ∃𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816
This theorem is referenced by:  spc2gv  3600  spc3egv  3603  spc2ev  3607  tpres  7221  addsrpr  11115  mulsrpr  11116  2pthon3v  29963  umgr2wlk  29969  0pthonv  30148  1pthon2v  30172  satfv1  35368  sat1el2xp  35384  dvnprodlem1  45961  dfatcolem  47267  fundcmpsurbijinj  47397
  Copyright terms: Public domain W3C validator