Step |
Hyp |
Ref |
Expression |
1 |
|
sbcssg |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐵 “ 𝐶 ) ⊆ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ 𝐶 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
2 |
|
csbima12 |
⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |
3 |
2
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
4 |
3
|
sseq1d |
⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 “ 𝐶 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
5 |
1 4
|
bitrd |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐵 “ 𝐶 ) ⊆ 𝐶 ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |
6 |
|
df-he |
⊢ ( 𝐵 hereditary 𝐶 ↔ ( 𝐵 “ 𝐶 ) ⊆ 𝐶 ) |
7 |
6
|
sbcbii |
⊢ ( [ 𝐴 / 𝑥 ] 𝐵 hereditary 𝐶 ↔ [ 𝐴 / 𝑥 ] ( 𝐵 “ 𝐶 ) ⊆ 𝐶 ) |
8 |
|
df-he |
⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 hereditary ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 “ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |
9 |
5 7 8
|
3bitr4g |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 hereditary 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 hereditary ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) |