Theorem rsp2e 2678

Description: Restricted specialization. (Contributed by FL, 4-Jun-2012.)

Assertion

Ref	Expression
rsp2e	⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃x ∈ A ∃y ∈ B φ)

Proof of Theorem rsp2e

Step	Hyp	Ref	Expression
1		simp1 955	. . 3 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → x ∈ A)
2		rspe 2676	. . . 4 ⊢ ((y ∈ B ∧ φ) → ∃y ∈ B φ)
3	2	3adant1 973	. . 3 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃y ∈ B φ)
4		19.8a 1756	. . 3 ⊢ ((x ∈ A ∧ ∃y ∈ B φ) → ∃x(x ∈ A ∧ ∃y ∈ B φ))
5	1, 3, 4	syl2anc 642	. 2 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃x(x ∈ A ∧ ∃y ∈ B φ))
6		df-rex 2621	. 2 ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x(x ∈ A ∧ ∃y ∈ B φ))
7	5, 6	sylibr 203	1 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) → ∃x ∈ A ∃y ∈ B φ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   ∈ wcel 1710  ∃wrex 2616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This proof depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-rex 2621

This theorem is used by: (None)