Step |
Hyp |
Ref |
Expression |
1 |
|
dfclel |
⊢ ( { 𝑥 ∣ 𝜑 } ∈ { 𝑦 ∣ 𝜓 } ↔ ∃ 𝑧 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ { 𝑦 ∣ 𝜓 } ) ) |
2 |
|
eliminable-veqab |
⊢ ( 𝑧 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ) |
3 |
|
eliminable-velab |
⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 ) |
4 |
2 3
|
anbi12i |
⊢ ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) ) |
5 |
4
|
exbii |
⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ { 𝑦 ∣ 𝜓 } ) ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) ) |
6 |
1 5
|
bitri |
⊢ ( { 𝑥 ∣ 𝜑 } ∈ { 𝑦 ∣ 𝜓 } ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) ) |