Metamath Proof Explorer

Theorem csbfrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024)

Ref Expression
Assertion csbfrecsg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , 𝐹 ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 csbuni ⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
2 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
3 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
4 sbc3an ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ∧ [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
5 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ↔ 𝑓 Fn 𝑧 ) )
6 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
7 sbcssg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
8 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑧 = 𝑧 )
9 8 sseq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ↔ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
10 7 9 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ↔ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
11 sbcralg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
12 sbcssg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ) )
13 csbpredg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) )
14 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
15 predeq3 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 → Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
16 14 15 syl ⊢ ( 𝐴 ∈ 𝑉 → Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
17 13 16 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
18 17 8 sseq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ↔ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
19 12 18 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
20 19 ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
21 11 20 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
22 10 21 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ) )
23 6 22 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ) )
24 sbcralg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
25 sbceqg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
26 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
27 csbov123 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) )
28 csbres ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑓 ↾ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) )
29 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑓 = 𝑓 )
30 29 17 reseq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑓 ↾ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) )
31 28 30 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) )
32 14 31 oveq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) )
33 27 32 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) )
34 26 33 eqeq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
35 25 34 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
36 35 ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
37 24 36 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
38 5 23 37 3anbi123d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ∧ [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
39 4 38 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
40 39 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
41 3 40 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
42 41 abbidv ⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
43 2 42 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
44 43 unieqd ⊢ ( 𝐴 ∈ 𝑉 → ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
45 1 44 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
46 df-frecs ⊢ frecs ( 𝑅 , 𝐷 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
47 46 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , 𝐹 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
48 df-frecs ⊢ frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) }
49 45 47 48 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , 𝐹 ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )