Theorem csbpredg

Description: Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csbpredg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		csbin	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) )
2		csbima12	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } )
3		csbcnv	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅
4	3	imaeq1i	⊢ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } )
5		csbsng	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } )
6	5	imaeq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
7	4 6	eqtr3id	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
8	2 7	syl5eq	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
9	8	ineq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) ) )
10	1 9	syl5eq	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) ) )
11		df-pred	⊢ Pred ( 𝑅 , 𝐷 , 𝑋 ) = ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
12	11	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
13		df-pred	⊢ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
14	10 12 13	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) )