Metamath Proof Explorer


Theorem sbcheg

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

Ref Expression
Assertion sbcheg A V [˙A / x]˙ B hereditary C A / x B hereditary A / x C

Proof

Step Hyp Ref Expression
1 sbcssg A V [˙A / x]˙ B C C A / x B C A / x C
2 csbima12 A / x B C = A / x B A / x C
3 2 a1i A V A / x B C = A / x B A / x C
4 3 sseq1d A V A / x B C A / x C A / x B A / x C A / x C
5 1 4 bitrd A V [˙A / x]˙ B C C A / x B A / x C A / x C
6 df-he B hereditary C B C C
7 6 sbcbii [˙A / x]˙ B hereditary C [˙A / x]˙ B C C
8 df-he A / x B hereditary A / x C A / x B A / x C A / x C
9 5 7 8 3bitr4g A V [˙A / x]˙ B hereditary C A / x B hereditary A / x C