Step |
Hyp |
Ref |
Expression |
1 |
|
bj-elabd2ALT.ex |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
bj-elabd2ALT.eq |
⊢ ( 𝜑 → 𝐵 = { 𝑥 ∣ 𝜓 } ) |
3 |
|
bj-elabd2ALT.is |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) ) |
4 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 ) |
5 |
2
|
eqcomd |
⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } = 𝐵 ) |
6 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → { 𝑥 ∣ 𝜓 } = 𝐵 ) |
7 |
4 6
|
eleq12d |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝐴 ∈ 𝐵 ) ) |
8 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) ) |
9 |
8
|
biimparc |
⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝐴 ) |
10 |
9
|
anim2i |
⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) ) → ( 𝜑 ∧ 𝑥 = 𝐴 ) ) |
11 |
10
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝜑 ∧ 𝑥 = 𝐴 ) ) |
12 |
11 3
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) |
13 |
12
|
sbiedvw |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜒 ) ) |
14 |
7 13
|
bibi12d |
⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) ) ) |
15 |
|
df-clab |
⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 ) |
16 |
15
|
a1i |
⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 ) ) |
17 |
1 14 16
|
vtocld |
⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) ) |