Metamath Proof Explorer

Theorem sbcfg

Description: Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Assertion sbcfg 
|- ( X e. V -> ( [. X / x ]. F : A --> B <-> [_ X / x ]_ F : [_ X / x ]_ A --> [_ X / x ]_ B ) )

Proof

Step Hyp Ref Expression
1 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2 1 a1i 
 |-  ( X e. V -> ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) )
3 2 sbcbidv 
 |-  ( X e. V -> ( [. X / x ]. F : A --> B <-> [. X / x ]. ( F Fn A /\ ran F C_ B ) ) )
4 sbcfng 
 |-  ( X e. V -> ( [. X / x ]. F Fn A <-> [_ X / x ]_ F Fn [_ X / x ]_ A ) )
5 sbcssg 
 |-  ( X e. V -> ( [. X / x ]. ran F C_ B <-> [_ X / x ]_ ran F C_ [_ X / x ]_ B ) )
6 csbrn 
 |-  [_ X / x ]_ ran F = ran [_ X / x ]_ F
7 6 sseq1i 
 |-  ( [_ X / x ]_ ran F C_ [_ X / x ]_ B <-> ran [_ X / x ]_ F C_ [_ X / x ]_ B )
8 5 7 bitrdi 
 |-  ( X e. V -> ( [. X / x ]. ran F C_ B <-> ran [_ X / x ]_ F C_ [_ X / x ]_ B ) )
9 4 8 anbi12d 
 |-  ( X e. V -> ( ( [. X / x ]. F Fn A /\ [. X / x ]. ran F C_ B ) <-> ( [_ X / x ]_ F Fn [_ X / x ]_ A /\ ran [_ X / x ]_ F C_ [_ X / x ]_ B ) ) )
10 sbcan 
 |-  ( [. X / x ]. ( F Fn A /\ ran F C_ B ) <-> ( [. X / x ]. F Fn A /\ [. X / x ]. ran F C_ B ) )
11 df-f 
 |-  ( [_ X / x ]_ F : [_ X / x ]_ A --> [_ X / x ]_ B <-> ( [_ X / x ]_ F Fn [_ X / x ]_ A /\ ran [_ X / x ]_ F C_ [_ X / x ]_ B ) )
12 9 10 11 3bitr4g 
 |-  ( X e. V -> ( [. X / x ]. ( F Fn A /\ ran F C_ B ) <-> [_ X / x ]_ F : [_ X / x ]_ A --> [_ X / x ]_ B ) )
13 3 12 bitrd 
 |-  ( X e. V -> ( [. X / x ]. F : A --> B <-> [_ X / x ]_ F : [_ X / x ]_ A --> [_ X / x ]_ B ) )