Step |
Hyp |
Ref |
Expression |
1 |
|
dfclel |
⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) |
2 |
1
|
a1i |
⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) ) |
3 |
|
vexwt |
⊢ ( ∀ 𝑥 𝜑 → 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) |
4 |
3
|
biantrud |
⊢ ( ∀ 𝑥 𝜑 → ( 𝑧 = 𝐴 ↔ ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) ) |
5 |
4
|
bicomd |
⊢ ( ∀ 𝑥 𝜑 → ( ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ 𝑧 = 𝐴 ) ) |
6 |
5
|
exbidv |
⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑧 𝑧 = 𝐴 ) ) |
7 |
|
bj-denotes |
⊢ ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) |
8 |
7
|
a1i |
⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) ) |
9 |
2 6 8
|
3bitrd |
⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 𝑦 = 𝐴 ) ) |