Step |
Hyp |
Ref |
Expression |
1 |
|
tfis.1 |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) ) |
2 |
|
ssrab2 |
⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On |
3 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
4 |
|
nfrab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝜑 } |
5 |
3 4
|
nfss |
⊢ Ⅎ 𝑥 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } |
6 |
4
|
nfcri |
⊢ Ⅎ 𝑥 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } |
7 |
5 6
|
nfim |
⊢ Ⅎ 𝑥 ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
8 |
|
dfss3 |
⊢ ( 𝑥 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
9 |
|
sseq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ) ) |
10 |
8 9
|
bitr3id |
⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ) ) |
11 |
|
rabid |
⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑥 ∈ On ∧ 𝜑 ) ) |
12 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) |
13 |
11 12
|
bitr3id |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ On ∧ 𝜑 ) ↔ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) |
14 |
10 13
|
imbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝑥 ∈ On ∧ 𝜑 ) ) ↔ ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) ) |
15 |
|
sbequ |
⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) |
16 |
|
nfcv |
⊢ Ⅎ 𝑥 On |
17 |
|
nfcv |
⊢ Ⅎ 𝑤 On |
18 |
|
nfv |
⊢ Ⅎ 𝑤 𝜑 |
19 |
|
nfs1v |
⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑 |
20 |
|
sbequ12 |
⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) ) |
21 |
16 17 18 19 20
|
cbvrabw |
⊢ { 𝑥 ∈ On ∣ 𝜑 } = { 𝑤 ∈ On ∣ [ 𝑤 / 𝑥 ] 𝜑 } |
22 |
15 21
|
elrab2 |
⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑦 ∈ On ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) |
23 |
22
|
simprbi |
⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → [ 𝑦 / 𝑥 ] 𝜑 ) |
24 |
23
|
ralimi |
⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) |
25 |
24 1
|
syl5 |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → 𝜑 ) ) |
26 |
25
|
anc2li |
⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝑥 ∈ On ∧ 𝜑 ) ) ) |
27 |
3 7 14 26
|
vtoclgaf |
⊢ ( 𝑧 ∈ On → ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) |
28 |
27
|
rgen |
⊢ ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) |
29 |
|
tfi |
⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) → { 𝑥 ∈ On ∣ 𝜑 } = On ) |
30 |
2 28 29
|
mp2an |
⊢ { 𝑥 ∈ On ∣ 𝜑 } = On |
31 |
30
|
eqcomi |
⊢ On = { 𝑥 ∈ On ∣ 𝜑 } |
32 |
31
|
rabeq2i |
⊢ ( 𝑥 ∈ On ↔ ( 𝑥 ∈ On ∧ 𝜑 ) ) |
33 |
32
|
simprbi |
⊢ ( 𝑥 ∈ On → 𝜑 ) |