This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2rspcedvdw

Description: Double application of rspcedvdw . (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses 2rspcedvdw.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2rspcedvdw.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
2rspcedvdw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
2rspcedvdw.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
2rspcedvdw.3 ⊢ ( 𝜑 → 𝜃 )
Assertion 2rspcedvdw ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝜓 )

Proof

Step Hyp Ref Expression
1 2rspcedvdw.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2 2rspcedvdw.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3 2rspcedvdw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
4 2rspcedvdw.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
5 2rspcedvdw.3 ⊢ ( 𝜑 → 𝜃 )
6 1 2 rspc2ev ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝜃 ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝜓 )
7 3 4 5 6 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑌 𝜓 )