Step |
Hyp |
Ref |
Expression |
1 |
|
opabssxpd.x |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 ) |
2 |
|
opabssxpd.y |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 ) |
3 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } |
4 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) → 𝑧 = 〈 𝑥 , 𝑦 〉 ) |
5 |
1 2
|
opelxpd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 〈 𝑥 , 𝑦 〉 ∈ ( 𝐴 × 𝐵 ) ) |
6 |
5
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) → 〈 𝑥 , 𝑦 〉 ∈ ( 𝐴 × 𝐵 ) ) |
7 |
4 6
|
eqeltrd |
⊢ ( ( 𝜑 ∧ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) |
8 |
7
|
ex |
⊢ ( 𝜑 → ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) ) |
9 |
8
|
exlimdvv |
⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) ) |
10 |
9
|
abssdv |
⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } ⊆ ( 𝐴 × 𝐵 ) ) |
11 |
3 10
|
eqsstrid |
⊢ ( 𝜑 → { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ ( 𝐴 × 𝐵 ) ) |