Metamath Proof Explorer

Theorem iscnrm3lem7

Description: Lemma for iscnrm3rlem8 and iscnrm3llem2 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Hypotheses iscnrm3lem7.1 ⊢ z = Z → χ ↔ θ
iscnrm3lem7.2 ⊢ w = W → θ ↔ τ
iscnrm3lem7.3 ⊢ φ ∧ x ∈ A ∧ y ∈ B ∧ ψ → Z ∈ C ∧ W ∈ D ∧ τ
Assertion iscnrm3lem7 ⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ → ∃ z ∈ C ∃ w ∈ D χ

Proof

Step Hyp Ref Expression
1 iscnrm3lem7.1 ⊢ z = Z → χ ↔ θ
2 iscnrm3lem7.2 ⊢ w = W → θ ↔ τ
3 iscnrm3lem7.3 ⊢ φ ∧ x ∈ A ∧ y ∈ B ∧ ψ → Z ∈ C ∧ W ∈ D ∧ τ
4 1 2 rspc2ev ⊢ Z ∈ C ∧ W ∈ D ∧ τ → ∃ z ∈ C ∃ w ∈ D χ
5 3 4 syl ⊢ φ ∧ x ∈ A ∧ y ∈ B ∧ ψ → ∃ z ∈ C ∃ w ∈ D χ
6 5 iscnrm3lem6 ⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ → ∃ z ∈ C ∃ w ∈ D χ