Theorem sbcfung

Description: Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017) Shorten proof and remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 12-Sep-2026)

	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 F\circ F^{-1}\subseteq \mathrm{I}\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}F\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\circ F^{-1}\subseteq \mathrm{I}\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		sbcssg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\circ F^{-1}\subseteq \mathrm{I}\leftrightarrow ⦋A/x⦌\left(F\circ F^{-1}\right)\subseteq ⦋A/x⦌\mathrm{I}\right)$$
4		csbcog	$$⊢A\in V\to ⦋A/x⦌\left(F\circ F^{-1}\right)=⦋A/x⦌F\circ ⦋A/x⦌F^{-1}$$
5		csbcnv	$$⊢{⦋A/x⦌F}^{-1}=⦋A/x⦌F^{-1}$$
6	5	coeq2i	$$⊢⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}=⦋A/x⦌F\circ ⦋A/x⦌F^{-1}$$
7	4 6	eqtr4di	$$⊢A\in V\to ⦋A/x⦌\left(F\circ F^{-1}\right)=⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}$$
8		csbconstg	$$⊢A\in V\to ⦋A/x⦌\mathrm{I}=\mathrm{I}$$
9	7 8	sseq12d	$$⊢A\in V\to \left(⦋A/x⦌\left(F\circ F^{-1}\right)\subseteq ⦋A/x⦌\mathrm{I}\leftrightarrow ⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}\subseteq \mathrm{I}\right)$$
10	3 9	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\circ F^{-1}\subseteq \mathrm{I}\leftrightarrow ⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}\subseteq \mathrm{I}\right)$$
11	2 10	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}F\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\circ F^{-1}\subseteq \mathrm{I}\right)\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge ⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}\subseteq \mathrm{I}\right)\right)$$
12	1 11	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\mathrm{Rel}F\wedge F\circ F^{-1}\subseteq \mathrm{I}\right)\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge ⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}\subseteq \mathrm{I}\right)\right)$$
13		df-fun	$$⊢\mathrm{Fun}F\leftrightarrow \left(\mathrm{Rel}F\wedge F\circ F^{-1}\subseteq \mathrm{I}\right)$$
14	13	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Fun}F\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\mathrm{Rel}F\wedge F\circ F^{-1}\subseteq \mathrm{I}\right)$$
15		df-fun	$$⊢\mathrm{Fun}⦋A/x⦌F\leftrightarrow \left(\mathrm{Rel}⦋A/x⦌F\wedge ⦋A/x⦌F\circ {⦋A/x⦌F}^{-1}\subseteq \mathrm{I}\right)$$
16	12 14 15	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Fun}F\leftrightarrow \mathrm{Fun}⦋A/x⦌F\right)$$