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 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧 ↔ 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 ) )
12 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 = 𝑦 ↔ 𝑧 = 𝑦 ) )
13 11 12 imbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑤 𝐹 𝑧 → [ 𝐴 / 𝑥 ] 𝑧 = 𝑦 ) ↔ ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
14 6 13 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
15 14 albidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
16 5 15 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
17 16 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
18 4 17 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
19 18 albidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
20 3 19 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
21 2 20 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] Rel 𝐹 ∧ [ 𝐴 / 𝑥 ] ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ) ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) ) )
22 1 21 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ) ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) ) )
23 dffun3 ⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
24 23 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ [ 𝐴 / 𝑥 ] ( Rel 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
25 dffun3 ⊢ ( Fun ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ↔ ( Rel ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∧ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( 𝑤 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 𝑧 → 𝑧 = 𝑦 ) ) )
26 22 24 25 3bitr4g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Fun 𝐹 ↔ Fun ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )