Step |
Hyp |
Ref |
Expression |
1 |
|
setinds.1 |
⊢ ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) |
2 |
|
vex |
⊢ 𝑥 ∈ V |
3 |
|
setind |
⊢ ( ∀ 𝑧 ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) → { 𝑥 ∣ 𝜑 } = V ) |
4 |
|
dfss3 |
⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
5 |
|
df-sbc |
⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
6 |
5
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
8 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 |
9 |
7 8
|
nfralw |
⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 |
10 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 |
11 |
9 10
|
nfim |
⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) |
12 |
|
raleq |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 ) ) |
13 |
|
sbceq1a |
⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) |
14 |
12 13
|
imbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ) ) |
15 |
11 14 1
|
chvarfv |
⊢ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) |
16 |
6 15
|
sylbir |
⊢ ( ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } → [ 𝑧 / 𝑥 ] 𝜑 ) |
17 |
4 16
|
sylbi |
⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → [ 𝑧 / 𝑥 ] 𝜑 ) |
18 |
|
df-sbc |
⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) |
19 |
17 18
|
sylib |
⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) |
20 |
3 19
|
mpg |
⊢ { 𝑥 ∣ 𝜑 } = V |
21 |
20
|
eqcomi |
⊢ V = { 𝑥 ∣ 𝜑 } |
22 |
21
|
abeq2i |
⊢ ( 𝑥 ∈ V ↔ 𝜑 ) |
23 |
2 22
|
mpbi |
⊢ 𝜑 |