Theorem spc2egv 3537

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

Step	Hyp	Ref	Expression
1		elisset 2821	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		elisset 2821	. . . 4 ⊢ (𝐵 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐵)
3	1, 2	anim12i 619	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4		exdistrv 1962	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
5	3, 4	sylibr 235	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))
6		spc2egv.1	. . . 4 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))
7	6	biimprcd 251	. . 3 ⊢ (𝜓 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜑))
8	7	2eximdv 1926	. 2 ⊢ (𝜓 → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ∃𝑥∃𝑦𝜑))
9	5, 8	syl5com 31	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-clel 2814

This theorem is referenced by:  spc2gv  3538  spc3egv  3541  spc2ev  3545  tpres  7145  addsrpr  10989  mulsrpr  10990  2pthon3v  30029  umgr2wlk  30035  0pthonv  30217  1pthon2v  30241  satfv1  35591  sat1el2xp  35607  dvnprodlem1  46389  dfatcolem  47718  fundcmpsurbijinj  47885  gpgprismgr4cyclex  48598