Theorem sbcfung

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

	Ref	Expression
Assertion	sbcfung	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Fun}F\leftrightarrow \mathrm{Fun}⦋A/x⦌F\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\mathrm{Rel}F\wedge \forall w\exists y\forall z\left(wFz\to z=y\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}F\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall w\exists y\forall z\left(wFz\to z=y\right)\right)$$
2		sbcrel	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}F\leftrightarrow \mathrm{Rel}⦋A/x⦌F\right)$$
3		sbcal	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall w\exists y\forall z\left(wFz\to z=y\right)\leftrightarrow \forall w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\forall z\left(wFz\to z=y\right)$$
4		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\forall z\left(wFz\to z=y\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\left(wFz\to z=y\right)$$
5		sbcal	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\left(wFz\to z=y\right)\leftrightarrow \forall z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(wFz\to z=y\right)$$
6		sbcimg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(wFz\to z=y\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}wFz\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=y\right)\right)$$
7		sbcbr123	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}wFz\leftrightarrow ⦋A/x⦌w⦋A/x⦌F⦋A/x⦌z$$
8		csbconstg	$$⊢A\in V\to ⦋A/x⦌w=w$$
9		csbconstg	$$⊢A\in V\to ⦋A/x⦌z=z$$
10	8 9	breq12d	$$⊢A\in V\to \left(⦋A/x⦌w⦋A/x⦌F⦋A/x⦌z\leftrightarrow w⦋A/x⦌Fz\right)$$
11	7 10	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}wFz\leftrightarrow w⦋A/x⦌Fz\right)$$
12		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=y\leftrightarrow z=y\right)$$
13	11 12	imbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}wFz\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=y\right)\leftrightarrow \left(w⦋A/x⦌Fz\to z=y\right)\right)$$
14	6 13	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(wFz\to z=y\right)\leftrightarrow \left(w⦋A/x⦌Fz\to z=y\right)\right)$$
15	14	albidv	$$⊢A\in V\to \left(\forall z\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(wFz\to z=y\right)\leftrightarrow \forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
16	5 15	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\left(wFz\to z=y\right)\leftrightarrow \forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
17	16	exbidv	$$⊢A\in V\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall z\left(wFz\to z=y\right)\leftrightarrow \exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
18	4 17	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\forall z\left(wFz\to z=y\right)\leftrightarrow \exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
19	18	albidv	$$⊢A\in V\to \left(\forall w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\forall z\left(wFz\to z=y\right)\leftrightarrow \forall w\exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
20	3 19	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall w\exists y\forall z\left(wFz\to z=y\right)\leftrightarrow \forall w\exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
21	2 20	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}F\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall w\exists y\forall z\left(wFz\to z=y\right)\right)\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge \forall w\exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)\right)$$
22	1 21	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\mathrm{Rel}F\wedge \forall w\exists y\forall z\left(wFz\to z=y\right)\right)\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge \forall w\exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)\right)$$
23		dffun3	$$⊢\mathrm{Fun}F\leftrightarrow \left(\mathrm{Rel}F\wedge \forall w\exists y\forall z\left(wFz\to z=y\right)\right)$$
24	23	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Fun}F\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\mathrm{Rel}F\wedge \forall w\exists y\forall z\left(wFz\to z=y\right)\right)$$
25		dffun3	$$⊢\mathrm{Fun}⦋A/x⦌F\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge \forall w\exists y\forall z\left(w⦋A/x⦌Fz\to z=y\right)\right)$$
26	22 24 25	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Fun}F\leftrightarrow \mathrm{Fun}⦋A/x⦌F\right)$$