Step |
Hyp |
Ref |
Expression |
1 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } |
2 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) } |
3 |
1 2
|
eqeq12i |
⊢ ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) ↔ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) } ) |
4 |
|
eqoprab2bw |
⊢ ( { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ) |
5 |
|
pm5.32 |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ) |
6 |
5
|
albii |
⊢ ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ↔ ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ) |
7 |
|
19.21v |
⊢ ( ∀ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
8 |
6 7
|
bitr3i |
⊢ ( ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
9 |
8
|
2albii |
⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
10 |
|
r2al |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
11 |
9 10
|
bitr4i |
⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐷 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) |
12 |
3 4 11
|
3bitri |
⊢ ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) |
13 |
|
pm13.183 |
⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 = 𝐷 ↔ ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
14 |
13
|
ralimi |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ∀ 𝑦 ∈ 𝐵 ( 𝐶 = 𝐷 ↔ ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
15 |
|
ralbi |
⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝐶 = 𝐷 ↔ ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) → ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
16 |
14 15
|
syl |
⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
17 |
16
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
18 |
|
ralbi |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
19 |
17 18
|
syl |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( 𝑧 = 𝐶 ↔ 𝑧 = 𝐷 ) ) ) |
20 |
12 19
|
bitr4id |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝐷 ) ) |