MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbfrecsg Structured version   Visualization version   GIF version

Theorem csbfrecsg 8290
Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024.)
Assertion
Ref Expression
csbfrecsg (𝐴𝑉𝐴 / 𝑥frecs(𝑅, 𝐷, 𝐹) = frecs(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝐹))

Proof of Theorem csbfrecsg
Dummy variables 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 csbuni 4939 . . 3 𝐴 / 𝑥 {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = 𝐴 / 𝑥{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))}
2 csbab 4438 . . . . 5 𝐴 / 𝑥{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓[𝐴 / 𝑥]𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))}
3 sbcex2 3841 . . . . . . 7 ([𝐴 / 𝑥]𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧[𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))))
4 sbc3an 3846 . . . . . . . . 9 ([𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ([𝐴 / 𝑥]𝑓 Fn 𝑧[𝐴 / 𝑥](𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ [𝐴 / 𝑥]𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))))
5 sbcg 3855 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥]𝑓 Fn 𝑧𝑓 Fn 𝑧))
6 sbcan 3829 . . . . . . . . . . 11 ([𝐴 / 𝑥](𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ ([𝐴 / 𝑥]𝑧𝐷[𝐴 / 𝑥]𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧))
7 sbcssg 4524 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝐷𝐴 / 𝑥𝑧𝐴 / 𝑥𝐷))
8 csbconstg 3911 . . . . . . . . . . . . . 14 (𝐴𝑉𝐴 / 𝑥𝑧 = 𝑧)
98sseq1d 4011 . . . . . . . . . . . . 13 (𝐴𝑉 → (𝐴 / 𝑥𝑧𝐴 / 𝑥𝐷𝑧𝐴 / 𝑥𝐷))
107, 9bitrd 279 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝐷𝑧𝐴 / 𝑥𝐷))
11 sbcralg 3867 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦𝑧 [𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧))
12 sbcssg 4524 . . . . . . . . . . . . . . 15 (𝐴𝑉 → ([𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦) ⊆ 𝐴 / 𝑥𝑧))
13 csbpredg 6311 . . . . . . . . . . . . . . . . 17 (𝐴𝑉𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦) = Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝑦))
14 csbconstg 3911 . . . . . . . . . . . . . . . . . 18 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
15 predeq3 6309 . . . . . . . . . . . . . . . . . 18 (𝐴 / 𝑥𝑦 = 𝑦 → Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝑦) = Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))
1614, 15syl 17 . . . . . . . . . . . . . . . . 17 (𝐴𝑉 → Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝑦) = Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))
1713, 16eqtrd 2768 . . . . . . . . . . . . . . . 16 (𝐴𝑉𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦) = Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))
1817, 8sseq12d 4013 . . . . . . . . . . . . . . 15 (𝐴𝑉 → (𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦) ⊆ 𝐴 / 𝑥𝑧 ↔ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧))
1912, 18bitrd 279 . . . . . . . . . . . . . 14 (𝐴𝑉 → ([𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧))
2019ralbidv 3174 . . . . . . . . . . . . 13 (𝐴𝑉 → (∀𝑦𝑧 [𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧))
2111, 20bitrd 279 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧))
2210, 21anbi12d 631 . . . . . . . . . . 11 (𝐴𝑉 → (([𝐴 / 𝑥]𝑧𝐷[𝐴 / 𝑥]𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧)))
236, 22bitrid 283 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧)))
24 sbcralg 3867 . . . . . . . . . . 11 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦𝑧 [𝐴 / 𝑥](𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))))
25 sbceqg 4410 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥](𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ 𝐴 / 𝑥(𝑓𝑦) = 𝐴 / 𝑥(𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))))
26 csbconstg 3911 . . . . . . . . . . . . . 14 (𝐴𝑉𝐴 / 𝑥(𝑓𝑦) = (𝑓𝑦))
27 csbov123 7462 . . . . . . . . . . . . . . 15 𝐴 / 𝑥(𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐹𝐴 / 𝑥(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))
28 csbres 5988 . . . . . . . . . . . . . . . . 17 𝐴 / 𝑥(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)) = (𝐴 / 𝑥𝑓𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦))
29 csbconstg 3911 . . . . . . . . . . . . . . . . . 18 (𝐴𝑉𝐴 / 𝑥𝑓 = 𝑓)
3029, 17reseq12d 5986 . . . . . . . . . . . . . . . . 17 (𝐴𝑉 → (𝐴 / 𝑥𝑓𝐴 / 𝑥Pred(𝑅, 𝐷, 𝑦)) = (𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))
3128, 30eqtrid 2780 . . . . . . . . . . . . . . . 16 (𝐴𝑉𝐴 / 𝑥(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)) = (𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))
3214, 31oveq12d 7438 . . . . . . . . . . . . . . 15 (𝐴𝑉 → (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐹𝐴 / 𝑥(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))
3327, 32eqtrid 2780 . . . . . . . . . . . . . 14 (𝐴𝑉𝐴 / 𝑥(𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))
3426, 33eqeq12d 2744 . . . . . . . . . . . . 13 (𝐴𝑉 → (𝐴 / 𝑥(𝑓𝑦) = 𝐴 / 𝑥(𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))))
3525, 34bitrd 279 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥](𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))))
3635ralbidv 3174 . . . . . . . . . . 11 (𝐴𝑉 → (∀𝑦𝑧 [𝐴 / 𝑥](𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))))
3724, 36bitrd 279 . . . . . . . . . 10 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦)))))
385, 23, 373anbi123d 1433 . . . . . . . . 9 (𝐴𝑉 → (([𝐴 / 𝑥]𝑓 Fn 𝑧[𝐴 / 𝑥](𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ [𝐴 / 𝑥]𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ (𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))))
394, 38bitrid 283 . . . . . . . 8 (𝐴𝑉 → ([𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ (𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))))
4039exbidv 1917 . . . . . . 7 (𝐴𝑉 → (∃𝑧[𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))))
413, 40bitrid 283 . . . . . 6 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))))
4241abbidv 2797 . . . . 5 (𝐴𝑉 → {𝑓[𝐴 / 𝑥]𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))})
432, 42eqtrid 2780 . . . 4 (𝐴𝑉𝐴 / 𝑥{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))})
4443unieqd 4921 . . 3 (𝐴𝑉 𝐴 / 𝑥{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))})
451, 44eqtrid 2780 . 2 (𝐴𝑉𝐴 / 𝑥 {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))})
46 df-frecs 8287 . . 3 frecs(𝑅, 𝐷, 𝐹) = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))}
4746csbeq2i 3900 . 2 𝐴 / 𝑥frecs(𝑅, 𝐷, 𝐹) = 𝐴 / 𝑥 {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐷 ∧ ∀𝑦𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))}
48 df-frecs 8287 . 2 frecs(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝐹) = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧𝐴 / 𝑥𝐷 ∧ ∀𝑦𝑧 Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦𝑧 (𝑓𝑦) = (𝑦𝐴 / 𝑥𝐹(𝑓 ↾ Pred(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝑦))))}
4945, 47, 483eqtr4g 2793 1 (𝐴𝑉𝐴 / 𝑥frecs(𝑅, 𝐷, 𝐹) = frecs(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wex 1774  wcel 2099  {cab 2705  wral 3058  [wsbc 3776  csb 3892  wss 3947   cuni 4908  cres 5680  Predcpred 6304   Fn wfn 6543  cfv 6548  (class class class)co 7420  frecscfrecs 8286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5684  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-iota 6500  df-fv 6556  df-ov 7423  df-frecs 8287
This theorem is referenced by:  csbwrecsg  8327
  Copyright terms: Public domain W3C validator