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 e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) )

Proof

Step	Hyp	Ref	Expression
1		sbcan	|- ( [. A / x ]. ( Rel F /\ ( F o. `' F ) C_ _I ) <-> ( [. A / x ]. Rel F /\ [. A / x ]. ( F o. `' F ) C_ _I ) )
2		sbcrel	|- ( A e. V -> ( [. A / x ]. Rel F <-> Rel [_ A / x ]_ F ) )
3		sbcssg	|- ( A e. V -> ( [. A / x ]. ( F o. `' F ) C_ _I <-> [_ A / x ]_ ( F o. `' F ) C_ [_ A / x ]_ _I ) )
4		csbcog	|- ( A e. V -> [_ A / x ]_ ( F o. `' F ) = ( [_ A / x ]_ F o. [_ A / x ]_ `' F ) )
5		csbcnv	|- `' [_ A / x ]_ F = [_ A / x ]_ `' F
6	5	coeq2i	|- ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) = ( [_ A / x ]_ F o. [_ A / x ]_ `' F )
7	4 6	eqtr4di	|- ( A e. V -> [_ A / x ]_ ( F o. `' F ) = ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) )
8		csbconstg	|- ( A e. V -> [_ A / x ]_ _I = _I )
9	7 8	sseq12d	|- ( A e. V -> ( [_ A / x ]_ ( F o. `' F ) C_ [_ A / x ]_ _I <-> ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) C_ _I ) )
10	3 9	bitrd	|- ( A e. V -> ( [. A / x ]. ( F o. `' F ) C_ _I <-> ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) C_ _I ) )
11	2 10	anbi12d	|- ( A e. V -> ( ( [. A / x ]. Rel F /\ [. A / x ]. ( F o. `' F ) C_ _I ) <-> ( Rel [_ A / x ]_ F /\ ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) C_ _I ) ) )
12	1 11	bitrid	|- ( A e. V -> ( [. A / x ]. ( Rel F /\ ( F o. `' F ) C_ _I ) <-> ( Rel [_ A / x ]_ F /\ ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) C_ _I ) ) )
13		df-fun	|- ( Fun F <-> ( Rel F /\ ( F o. `' F ) C_ _I ) )
14	13	sbcbii	|- ( [. A / x ]. Fun F <-> [. A / x ]. ( Rel F /\ ( F o. `' F ) C_ _I ) )
15		df-fun	|- ( Fun [_ A / x ]_ F <-> ( Rel [_ A / x ]_ F /\ ( [_ A / x ]_ F o. `' [_ A / x ]_ F ) C_ _I ) )
16	12 14 15	3bitr4g	|- ( A e. V -> ( [. A / x ]. Fun F <-> Fun [_ A / x ]_ F ) )