Description: Lemma for iscnrm3rlem8 and iscnrm3llem2 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iscnrm3lem7.1 | ⊢ ( 𝑧 = 𝑍 → ( 𝜒 ↔ 𝜃 ) ) | |
iscnrm3lem7.2 | ⊢ ( 𝑤 = 𝑊 → ( 𝜃 ↔ 𝜏 ) ) | ||
iscnrm3lem7.3 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) ) | ||
Assertion | iscnrm3lem7 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscnrm3lem7.1 | ⊢ ( 𝑧 = 𝑍 → ( 𝜒 ↔ 𝜃 ) ) | |
2 | iscnrm3lem7.2 | ⊢ ( 𝑤 = 𝑊 → ( 𝜃 ↔ 𝜏 ) ) | |
3 | iscnrm3lem7.3 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) ) | |
4 | 1 2 | rspc2ev | ⊢ ( ( 𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏 ) → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) |
5 | 3 4 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) |
6 | 5 | iscnrm3lem6 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 𝜒 ) ) |