Step |
Hyp |
Ref |
Expression |
1 |
|
elopab |
⊢ ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 〈 𝐴 , 𝐵 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
2 |
|
19.26-2 |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) ) |
3 |
|
anim12 |
⊢ ( ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜓 ↔ 𝜒 ) ) ) ) |
4 |
|
bitr |
⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜓 ↔ 𝜒 ) ) → ( 𝜑 ↔ 𝜒 ) ) |
5 |
3 4
|
syl6 |
⊢ ( ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) ) |
6 |
5
|
2alimi |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) ) |
7 |
2 6
|
sylbir |
⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) ) |
8 |
|
copsex2t |
⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 〈 𝐴 , 𝐵 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ 𝜒 ) ) |
9 |
7 8
|
stoic3 |
⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 〈 𝐴 , 𝐵 〉 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ 𝜒 ) ) |
10 |
1 9
|
syl5bb |
⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( 〈 𝐴 , 𝐵 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ 𝜒 ) ) |