Metamath Proof Explorer


Theorem csbpredg

Description: Move class substitution in and out of the predecessor class of a relation. (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 eqtrid ( 𝐴𝑉 𝐴 / 𝑥 ( 𝑅 “ { 𝑋 } ) = ( 𝐴 / 𝑥 𝑅 “ { 𝐴 / 𝑥 𝑋 } ) )
9 8 ineq2d ( 𝐴𝑉 → ( 𝐴 / 𝑥 𝐷 𝐴 / 𝑥 ( 𝑅 “ { 𝑋 } ) ) = ( 𝐴 / 𝑥 𝐷 ∩ ( 𝐴 / 𝑥 𝑅 “ { 𝐴 / 𝑥 𝑋 } ) ) )
10 1 9 eqtrid ( 𝐴𝑉 𝐴 / 𝑥 ( 𝐷 ∩ ( 𝑅 “ { 𝑋 } ) ) = ( 𝐴 / 𝑥 𝐷 ∩ ( 𝐴 / 𝑥 𝑅 “ { 𝐴 / 𝑥 𝑋 } ) ) )
11 df-pred Pred ( 𝑅 , 𝐷 , 𝑋 ) = ( 𝐷 ∩ ( 𝑅 “ { 𝑋 } ) )
12 11 csbeq2i 𝐴 / 𝑥 Pred ( 𝑅 , 𝐷 , 𝑋 ) = 𝐴 / 𝑥 ( 𝐷 ∩ ( 𝑅 “ { 𝑋 } ) )
13 df-pred Pred ( 𝐴 / 𝑥 𝑅 , 𝐴 / 𝑥 𝐷 , 𝐴 / 𝑥 𝑋 ) = ( 𝐴 / 𝑥 𝐷 ∩ ( 𝐴 / 𝑥 𝑅 “ { 𝐴 / 𝑥 𝑋 } ) )
14 10 12 13 3eqtr4g ( 𝐴𝑉 𝐴 / 𝑥 Pred ( 𝑅 , 𝐷 , 𝑋 ) = Pred ( 𝐴 / 𝑥 𝑅 , 𝐴 / 𝑥 𝐷 , 𝐴 / 𝑥 𝑋 ) )