# 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 syl5bb
` |-  ( 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 syl5bb
` |-  ( 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 syl5bb
` |-  ( 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 syl5bb
` |-  ( 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 syl5bb
` |-  ( 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 ) )`