Step |
Hyp |
Ref |
Expression |
1 |
|
dmrab.1 |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
1
|
elrab |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( 〈 𝑥 , 𝑦 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜓 ) ) |
3 |
|
opelxp |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
4 |
3
|
anbi1i |
⊢ ( ( 〈 𝑥 , 𝑦 〉 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ) |
5 |
|
ancom |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) |
6 |
5
|
anbi1i |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) ) |
7 |
2 4 6
|
3bitri |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) ) |
8 |
|
anass |
⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) |
9 |
|
ancom |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) |
10 |
9
|
anbi2i |
⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) ) |
11 |
7 8 10
|
3bitri |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) ) |
12 |
11
|
exbii |
⊢ ( ∃ 𝑦 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) ) |
13 |
|
df-rex |
⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) ) |
14 |
|
r19.41v |
⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜓 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) |
15 |
12 13 14
|
3bitr2i |
⊢ ( ∃ 𝑦 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( ∃ 𝑦 ∈ 𝐵 𝜓 ∧ 𝑥 ∈ 𝐴 ) ) |
16 |
15
|
biancomi |
⊢ ( ∃ 𝑦 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) ) |
17 |
16
|
abbii |
⊢ { 𝑥 ∣ ∃ 𝑦 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) } |
18 |
|
dfdm3 |
⊢ dom { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 〈 𝑥 , 𝑦 〉 ∈ { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } } |
19 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜓 ) } |
20 |
17 18 19
|
3eqtr4i |
⊢ dom { 𝑧 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 ∈ 𝐵 𝜓 } |