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	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ Fun ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) ↔ ( [ 𝐴 / 𝑥 ] Rel 𝐹 ∧ [ 𝐴 / 𝑥 ] ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
2		sbcrel	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Rel 𝐹 ↔ Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
3		sbcssg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ I ) )
4		csbcog	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ ◡ 𝐹 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 ) )
5		csbcnv	⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹
6	5	coeq2i	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝐹 )
7	4 6	eqtr4di	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ ◡ 𝐹 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )
8		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ I = I )
9	7 8	sseq12d	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ I ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) ⊆ I ) )
10	3 9	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) ⊆ I ) )
11	2 10	anbi12d	⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] Rel 𝐹 ∧ [ 𝐴 / 𝑥 ] ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) ⊆ I ) ) )
12	1 11	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) ⊆ I ) ) )
13		df-fun	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
14	13	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
15		df-fun	⊢ ( Fun ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) ⊆ I ) )
16	12 14 15	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ Fun ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )