Theorem sbcheg

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

	Ref	Expression
Assertion	sbcheg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BhereditaryC\leftrightarrow ⦋A/x⦌Bhereditary⦋A/x⦌C\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcssg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\left[C\right]\subseteq C\leftrightarrow ⦋A/x⦌B\left[C\right]\subseteq ⦋A/x⦌C\right)$$
2		csbima12	$$⊢⦋A/x⦌B\left[C\right]=⦋A/x⦌B\left[⦋A/x⦌C\right]$$
3	2	a1i	$$⊢A\in V\to ⦋A/x⦌B\left[C\right]=⦋A/x⦌B\left[⦋A/x⦌C\right]$$
4	3	sseq1d	$$⊢A\in V\to \left(⦋A/x⦌B\left[C\right]\subseteq ⦋A/x⦌C\leftrightarrow ⦋A/x⦌B\left[⦋A/x⦌C\right]\subseteq ⦋A/x⦌C\right)$$
5	1 4	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\left[C\right]\subseteq C\leftrightarrow ⦋A/x⦌B\left[⦋A/x⦌C\right]\subseteq ⦋A/x⦌C\right)$$
6		df-he	$$⊢BhereditaryC\leftrightarrow B\left[C\right]\subseteq C$$
7	6	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BhereditaryC\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\left[C\right]\subseteq C$$
8		df-he	$$⊢⦋A/x⦌Bhereditary⦋A/x⦌C\leftrightarrow ⦋A/x⦌B\left[⦋A/x⦌C\right]\subseteq ⦋A/x⦌C$$
9	5 7 8	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BhereditaryC\leftrightarrow ⦋A/x⦌Bhereditary⦋A/x⦌C\right)$$