Theorem sbcheg

Description: Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020)

	Ref	Expression
Assertion	sbcheg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 hereditary 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 hereditary ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

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 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )