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∈V→[˙A/x]˙Fun⁡F↔Fun⁡⦋A/x⦌F

Proof

Step Hyp Ref Expression
1 sbcan ⊢[˙A/x]˙Rel⁡F∧∀w∃y∀zwFz→z=y↔[˙A/x]˙Rel⁡F∧[˙A/x]˙∀w∃y∀zwFz→z=y
2 sbcrel ⊢A∈V→[˙A/x]˙Rel⁡F↔Rel⁡⦋A/x⦌F
3 sbcal ⊢[˙A/x]˙∀w∃y∀zwFz→z=y↔∀w[˙A/x]˙∃y∀zwFz→z=y
4 sbcex2 ⊢[˙A/x]˙∃y∀zwFz→z=y↔∃y[˙A/x]˙∀zwFz→z=y
5 sbcal ⊢[˙A/x]˙∀zwFz→z=y↔∀z[˙A/x]˙wFz→z=y
6 sbcimg ⊢A∈V→[˙A/x]˙wFz→z=y↔[˙A/x]˙wFz→[˙A/x]˙z=y
7 sbcbr123 ⊢[˙A/x]˙wFz↔⦋A/x⦌w⦋A/x⦌F⦋A/x⦌z
8 csbconstg ⊢A∈V→⦋A/x⦌w=w
9 csbconstg ⊢A∈V→⦋A/x⦌z=z
10 8 9 breq12d ⊢A∈V→⦋A/x⦌w⦋A/x⦌F⦋A/x⦌z↔w⦋A/x⦌Fz
11 7 10 bitrid ⊢A∈V→[˙A/x]˙wFz↔w⦋A/x⦌Fz
12 sbcg ⊢A∈V→[˙A/x]˙z=y↔z=y
13 11 12 imbi12d ⊢A∈V→[˙A/x]˙wFz→[˙A/x]˙z=y↔w⦋A/x⦌Fz→z=y
14 6 13 bitrd ⊢A∈V→[˙A/x]˙wFz→z=y↔w⦋A/x⦌Fz→z=y
15 14 albidv ⊢A∈V→∀z[˙A/x]˙wFz→z=y↔∀zw⦋A/x⦌Fz→z=y
16 5 15 bitrid ⊢A∈V→[˙A/x]˙∀zwFz→z=y↔∀zw⦋A/x⦌Fz→z=y
17 16 exbidv ⊢A∈V→∃y[˙A/x]˙∀zwFz→z=y↔∃y∀zw⦋A/x⦌Fz→z=y
18 4 17 bitrid ⊢A∈V→[˙A/x]˙∃y∀zwFz→z=y↔∃y∀zw⦋A/x⦌Fz→z=y
19 18 albidv ⊢A∈V→∀w[˙A/x]˙∃y∀zwFz→z=y↔∀w∃y∀zw⦋A/x⦌Fz→z=y
20 3 19 bitrid ⊢A∈V→[˙A/x]˙∀w∃y∀zwFz→z=y↔∀w∃y∀zw⦋A/x⦌Fz→z=y
21 2 20 anbi12d ⊢A∈V→[˙A/x]˙Rel⁡F∧[˙A/x]˙∀w∃y∀zwFz→z=y↔Rel⁡⦋A/x⦌F∧∀w∃y∀zw⦋A/x⦌Fz→z=y
22 1 21 bitrid ⊢A∈V→[˙A/x]˙Rel⁡F∧∀w∃y∀zwFz→z=y↔Rel⁡⦋A/x⦌F∧∀w∃y∀zw⦋A/x⦌Fz→z=y
23 dffun3 ⊢Fun⁡F↔Rel⁡F∧∀w∃y∀zwFz→z=y
24 23 sbcbii ⊢[˙A/x]˙Fun⁡F↔[˙A/x]˙Rel⁡F∧∀w∃y∀zwFz→z=y
25 dffun3 ⊢Fun⁡⦋A/x⦌F↔Rel⁡⦋A/x⦌F∧∀w∃y∀zw⦋A/x⦌Fz→z=y
26 22 24 25 3bitr4g ⊢A∈V→[˙A/x]˙Fun⁡F↔Fun⁡⦋A/x⦌F