Metamath Proof Explorer

Theorem sbcfung

Description: Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion sbcfung 
|- ( A e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) )

Proof

Step Hyp Ref Expression
1 sbcan 
 |-  ( [. A / x ]. ( Rel F /\ A. w E. y A. z ( w F z -> z = y ) ) <-> ( [. A / x ]. Rel F /\ [. A / x ]. A. w E. y A. z ( w F z -> z = y ) ) )
2 sbcrel 
 |-  ( A e. V -> ( [. A / x ]. Rel F <-> Rel [_ A / x ]_ F ) )
3 sbcal 
 |-  ( [. A / x ]. A. w E. y A. z ( w F z -> z = y ) <-> A. w [. A / x ]. E. y A. z ( w F z -> z = y ) )
4 sbcex2 
 |-  ( [. A / x ]. E. y A. z ( w F z -> z = y ) <-> E. y [. A / x ]. A. z ( w F z -> z = y ) )
5 sbcal 
 |-  ( [. A / x ]. A. z ( w F z -> z = y ) <-> A. z [. A / x ]. ( w F z -> z = y ) )
6 sbcimg 
 |-  ( A e. V -> ( [. A / x ]. ( w F z -> z = y ) <-> ( [. A / x ]. w F z -> [. A / x ]. z = y ) ) )
7 sbcbr123 
 |-  ( [. A / x ]. w F z <-> [_ A / x ]_ w [_ A / x ]_ F [_ A / x ]_ z )
8 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ w = w )
9 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ z = z )
10 8 9 breq12d 
 |-  ( A e. V -> ( [_ A / x ]_ w [_ A / x ]_ F [_ A / x ]_ z <-> w [_ A / x ]_ F z ) )
11 7 10 bitrid 
 |-  ( A e. V -> ( [. A / x ]. w F z <-> w [_ A / x ]_ F z ) )
12 sbcg 
 |-  ( A e. V -> ( [. A / x ]. z = y <-> z = y ) )
13 11 12 imbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. w F z -> [. A / x ]. z = y ) <-> ( w [_ A / x ]_ F z -> z = y ) ) )
14 6 13 bitrd 
 |-  ( A e. V -> ( [. A / x ]. ( w F z -> z = y ) <-> ( w [_ A / x ]_ F z -> z = y ) ) )
15 14 albidv 
 |-  ( A e. V -> ( A. z [. A / x ]. ( w F z -> z = y ) <-> A. z ( w [_ A / x ]_ F z -> z = y ) ) )
16 5 15 bitrid 
 |-  ( A e. V -> ( [. A / x ]. A. z ( w F z -> z = y ) <-> A. z ( w [_ A / x ]_ F z -> z = y ) ) )
17 16 exbidv 
 |-  ( A e. V -> ( E. y [. A / x ]. A. z ( w F z -> z = y ) <-> E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) )
18 4 17 bitrid 
 |-  ( A e. V -> ( [. A / x ]. E. y A. z ( w F z -> z = y ) <-> E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) )
19 18 albidv 
 |-  ( A e. V -> ( A. w [. A / x ]. E. y A. z ( w F z -> z = y ) <-> A. w E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) )
20 3 19 bitrid 
 |-  ( A e. V -> ( [. A / x ]. A. w E. y A. z ( w F z -> z = y ) <-> A. w E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) )
21 2 20 anbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. Rel F /\ [. A / x ]. A. w E. y A. z ( w F z -> z = y ) ) <-> ( Rel [_ A / x ]_ F /\ A. w E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) ) )
22 1 21 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( Rel F /\ A. w E. y A. z ( w F z -> z = y ) ) <-> ( Rel [_ A / x ]_ F /\ A. w E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) ) )
23 dffun3 
 |-  ( Fun F <-> ( Rel F /\ A. w E. y A. z ( w F z -> z = y ) ) )
24 23 sbcbii 
 |-  ( [. A / x ]. Fun F <-> [. A / x ]. ( Rel F /\ A. w E. y A. z ( w F z -> z = y ) ) )
25 dffun3 
 |-  ( Fun [_ A / x ]_ F <-> ( Rel [_ A / x ]_ F /\ A. w E. y A. z ( w [_ A / x ]_ F z -> z = y ) ) )
26 22 24 25 3bitr4g 
 |-  ( A e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) )