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

Proof

Step Hyp Ref Expression
1 sbcan ( [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) ↔ ( [ 𝐴 / 𝑥 ] Rel 𝐹[ 𝐴 / 𝑥 ]𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) )
2 sbcrel ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] Rel 𝐹 ↔ Rel 𝐴 / 𝑥 𝐹 ) )
3 sbcal ( [ 𝐴 / 𝑥 ]𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑤 [ 𝐴 / 𝑥 ]𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) )
4 sbcex2 ( [ 𝐴 / 𝑥 ]𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ]𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) )
5 sbcal ( [ 𝐴 / 𝑥 ]𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) )
6 sbcimg ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧[ 𝐴 / 𝑥 ] 𝑧 = 𝑦 ) ) )
7 sbcbr123 ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧 𝐴 / 𝑥 𝑤 𝐴 / 𝑥 𝐹 𝐴 / 𝑥 𝑧 )
8 csbconstg ( 𝐴𝑉 𝐴 / 𝑥 𝑤 = 𝑤 )
9 csbconstg ( 𝐴𝑉 𝐴 / 𝑥 𝑧 = 𝑧 )
10 8 9 breq12d ( 𝐴𝑉 → ( 𝐴 / 𝑥 𝑤 𝐴 / 𝑥 𝐹 𝐴 / 𝑥 𝑧𝑤 𝐴 / 𝑥 𝐹 𝑧 ) )
11 7 10 syl5bb ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧𝑤 𝐴 / 𝑥 𝐹 𝑧 ) )
12 sbcg ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 = 𝑦𝑧 = 𝑦 ) )
13 11 12 imbi12d ( 𝐴𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧[ 𝐴 / 𝑥 ] 𝑧 = 𝑦 ) ↔ ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
14 6 13 bitrd ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
15 14 albidv ( 𝐴𝑉 → ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
16 5 15 syl5bb ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ]𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
17 16 exbidv ( 𝐴𝑉 → ( ∃ 𝑦 [ 𝐴 / 𝑥 ]𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∃ 𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
18 4 17 syl5bb ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ]𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∃ 𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
19 18 albidv ( 𝐴𝑉 → ( ∀ 𝑤 [ 𝐴 / 𝑥 ]𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
20 3 19 syl5bb ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ]𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ↔ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
21 2 20 anbi12d ( 𝐴𝑉 → ( ( [ 𝐴 / 𝑥 ] Rel 𝐹[ 𝐴 / 𝑥 ]𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) ↔ ( Rel 𝐴 / 𝑥 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) ) )
22 1 21 syl5bb ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) ↔ ( Rel 𝐴 / 𝑥 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) ) )
23 dffun3 ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) )
24 23 sbcbii ( [ 𝐴 / 𝑥 ] Fun 𝐹[ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐹 𝑧𝑧 = 𝑦 ) ) )
25 dffun3 ( Fun 𝐴 / 𝑥 𝐹 ↔ ( Rel 𝐴 / 𝑥 𝐹 ∧ ∀ 𝑤𝑦𝑧 ( 𝑤 𝐴 / 𝑥 𝐹 𝑧𝑧 = 𝑦 ) ) )
26 22 24 25 3bitr4g ( 𝐴𝑉 → ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ Fun 𝐴 / 𝑥 𝐹 ) )