Metamath Proof Explorer


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