Step |
Hyp |
Ref |
Expression |
1 |
|
mpomptx2.1 |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → 𝐶 = 𝐷 ) |
2 |
|
df-mpt |
⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↦ 𝐶 ) = { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) } |
3 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) } |
4 |
|
eliunxp2 |
⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) |
5 |
4
|
anbi1i |
⊢ ( ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ) |
6 |
|
19.41vv |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ) |
7 |
|
anass |
⊢ ( ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ) |
8 |
1
|
eqeq2d |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( 𝑤 = 𝐶 ↔ 𝑤 = 𝐷 ) ) |
9 |
8
|
anbi2d |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) ) |
10 |
9
|
pm5.32i |
⊢ ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ↔ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) ) |
11 |
7 10
|
bitri |
⊢ ( ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) ) |
12 |
11
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) ) |
13 |
5 6 12
|
3bitr2i |
⊢ ( ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) ) |
14 |
13
|
opabbii |
⊢ { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) } = { 〈 𝑧 , 𝑤 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) } |
15 |
|
dfoprab2 |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) } = { 〈 𝑧 , 𝑤 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) } |
16 |
14 15
|
eqtr4i |
⊢ { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑤 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) } |
17 |
3 16
|
eqtr4i |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) } |
18 |
2 17
|
eqtr4i |
⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) |