Step |
Hyp |
Ref |
Expression |
1 |
|
dmoprab |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } |
2 |
|
19.42v |
⊢ ( ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 𝜑 ) ) |
3 |
2
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 𝜑 ) } |
4 |
|
opabssxp |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑧 𝜑 ) } ⊆ ( 𝐴 × 𝐵 ) |
5 |
3 4
|
eqsstri |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 ) |
6 |
1 5
|
eqsstri |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 ) |