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

Theorem spc2egv 3548
 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 3452 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 elisset 3452 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
31, 2anim12i 615 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4 exdistrv 1956 . . 3 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
53, 4sylibr 237 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵))
6 spc2egv.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
76biimprcd 253 . . 3 (𝜓 → ((𝑥 = 𝐴𝑦 = 𝐵) → 𝜑))
872eximdv 1920 . 2 (𝜓 → (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → ∃𝑥𝑦𝜑))
95, 8syl5com 31 1 ((𝐴𝑉𝐵𝑊) → (𝜓 → ∃𝑥𝑦𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870 This theorem is referenced by:  spc2gv  3549  spc3egv  3552  spc2ev  3556  tpres  6941  addsrpr  10489  mulsrpr  10490  2pthon3v  27739  umgr2wlk  27745  0pthonv  27924  1pthon2v  27948  satfv1  32738  sat1el2xp  32754  dvnprodlem1  42631  dfatcolem  43854  fundcmpsurbijinj  43970
 Copyright terms: Public domain W3C validator