Step |
Hyp |
Ref |
Expression |
1 |
|
ssopab2b |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ) |
2 |
|
ssopab2b |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) ) |
3 |
1 2
|
anbi12i |
⊢ ( ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∧ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) ) ) |
4 |
|
eqss |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ↔ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ∧ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) ) |
5 |
|
2albiim |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) ) ) |
6 |
3 4 5
|
3bitr4i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ 𝜓 ) ) |