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

Theorem spc2egv 3588
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 2813 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 elisset 2813 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
31, 2anim12i 611 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4 exdistrv 1957 . . 3 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
53, 4sylibr 233 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵))
6 spc2egv.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
76biimprcd 249 . . 3 (𝜓 → ((𝑥 = 𝐴𝑦 = 𝐵) → 𝜑))
872eximdv 1920 . 2 (𝜓 → (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → ∃𝑥𝑦𝜑))
95, 8syl5com 31 1 ((𝐴𝑉𝐵𝑊) → (𝜓 → ∃𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wex 1779  wcel 2104
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 1911  ax-6 1969  ax-7 2009  ax-8 2106
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2808
This theorem is referenced by:  spc2gv  3589  spc3egv  3592  spc2ev  3596  tpres  7203  addsrpr  11072  mulsrpr  11073  2pthon3v  29464  umgr2wlk  29470  0pthonv  29649  1pthon2v  29673  satfv1  34652  sat1el2xp  34668  dvnprodlem1  44960  dfatcolem  46261  fundcmpsurbijinj  46376
  Copyright terms: Public domain W3C validator