This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcfng

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

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

Proof

Step Hyp Ref Expression
1 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
2 1 a1i 
 |-  ( X e. V -> ( F Fn A <-> ( Fun F /\ dom F = A ) ) )
3 2 sbcbidv 
 |-  ( X e. V -> ( [. X / x ]. F Fn A <-> [. X / x ]. ( Fun F /\ dom F = A ) ) )
4 sbcfung 
 |-  ( X e. V -> ( [. X / x ]. Fun F <-> Fun [_ X / x ]_ F ) )
5 sbceqg 
 |-  ( X e. V -> ( [. X / x ]. dom F = A <-> [_ X / x ]_ dom F = [_ X / x ]_ A ) )
6 csbdm 
 |-  [_ X / x ]_ dom F = dom [_ X / x ]_ F
7 6 eqeq1i 
 |-  ( [_ X / x ]_ dom F = [_ X / x ]_ A <-> dom [_ X / x ]_ F = [_ X / x ]_ A )
8 5 7 bitrdi 
 |-  ( X e. V -> ( [. X / x ]. dom F = A <-> dom [_ X / x ]_ F = [_ X / x ]_ A ) )
9 4 8 anbi12d 
 |-  ( X e. V -> ( ( [. X / x ]. Fun F /\ [. X / x ]. dom F = A ) <-> ( Fun [_ X / x ]_ F /\ dom [_ X / x ]_ F = [_ X / x ]_ A ) ) )
10 sbcan 
 |-  ( [. X / x ]. ( Fun F /\ dom F = A ) <-> ( [. X / x ]. Fun F /\ [. X / x ]. dom F = A ) )
11 df-fn 
 |-  ( [_ X / x ]_ F Fn [_ X / x ]_ A <-> ( Fun [_ X / x ]_ F /\ dom [_ X / x ]_ F = [_ X / x ]_ A ) )
12 9 10 11 3bitr4g 
 |-  ( X e. V -> ( [. X / x ]. ( Fun F /\ dom F = A ) <-> [_ X / x ]_ F Fn [_ X / x ]_ A ) )
13 3 12 bitrd 
 |-  ( X e. V -> ( [. X / x ]. F Fn A <-> [_ X / x ]_ F Fn [_ X / x ]_ A ) )