Theorem sbcheg

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

	Ref	Expression
Assertion	sbcheg	|- ( A e. V -> ( [. A / x ]. B hereditary C <-> [_ A / x ]_ B hereditary [_ A / x ]_ C ) )

Proof

Step	Hyp	Ref	Expression
1		sbcssg	|- ( A e. V -> ( [. A / x ]. ( B " C ) C_ C <-> [_ A / x ]_ ( B " C ) C_ [_ A / x ]_ C ) )
2		csbima12	|- [_ A / x ]_ ( B " C ) = ( [_ A / x ]_ B " [_ A / x ]_ C )
3	2	a1i	|- ( A e. V -> [_ A / x ]_ ( B " C ) = ( [_ A / x ]_ B " [_ A / x ]_ C ) )
4	3	sseq1d	|- ( A e. V -> ( [_ A / x ]_ ( B " C ) C_ [_ A / x ]_ C <-> ( [_ A / x ]_ B " [_ A / x ]_ C ) C_ [_ A / x ]_ C ) )
5	1 4	bitrd	|- ( A e. V -> ( [. A / x ]. ( B " C ) C_ C <-> ( [_ A / x ]_ B " [_ A / x ]_ C ) C_ [_ A / x ]_ C ) )
6		df-he	|- ( B hereditary C <-> ( B " C ) C_ C )
7	6	sbcbii	|- ( [. A / x ]. B hereditary C <-> [. A / x ]. ( B " C ) C_ C )
8		df-he	|- ( [_ A / x ]_ B hereditary [_ A / x ]_ C <-> ( [_ A / x ]_ B " [_ A / x ]_ C ) C_ [_ A / x ]_ C )
9	5 7 8	3bitr4g	|- ( A e. V -> ( [. A / x ]. B hereditary C <-> [_ A / x ]_ B hereditary [_ A / x ]_ C ) )