![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > recseq | GIF version |
Description: Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
Ref | Expression |
---|---|
recseq | ⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq1 5428 | . . . . . . . 8 ⊢ (𝐹 = 𝐺 → (𝐹‘(𝑎 ↾ 𝑐)) = (𝐺‘(𝑎 ↾ 𝑐))) | |
2 | 1 | eqeq2d 2152 | . . . . . . 7 ⊢ (𝐹 = 𝐺 → ((𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))) |
3 | 2 | ralbidv 2438 | . . . . . 6 ⊢ (𝐹 = 𝐺 → (∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))) |
4 | 3 | anbi2d 460 | . . . . 5 ⊢ (𝐹 = 𝐺 → ((𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))) |
5 | 4 | rexbidv 2439 | . . . 4 ⊢ (𝐹 = 𝐺 → (∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐))) ↔ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))) |
6 | 5 | abbidv 2258 | . . 3 ⊢ (𝐹 = 𝐺 → {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐)))} = {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))}) |
7 | 6 | unieqd 3755 | . 2 ⊢ (𝐹 = 𝐺 → ∪ {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐)))} = ∪ {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))}) |
8 | df-recs 6210 | . 2 ⊢ recs(𝐹) = ∪ {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐹‘(𝑎 ↾ 𝑐)))} | |
9 | df-recs 6210 | . 2 ⊢ recs(𝐺) = ∪ {𝑎 ∣ ∃𝑏 ∈ On (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))} | |
10 | 7, 8, 9 | 3eqtr4g 2198 | 1 ⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1332 {cab 2126 ∀wral 2417 ∃wrex 2418 ∪ cuni 3744 Oncon0 4293 ↾ cres 4549 Fn wfn 5126 ‘cfv 5131 recscrecs 6209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 df-rex 2423 df-uni 3745 df-br 3938 df-iota 5096 df-fv 5139 df-recs 6210 |
This theorem is referenced by: rdgeq1 6276 rdgeq2 6277 freceq1 6297 freceq2 6298 frecsuclem 6311 |
Copyright terms: Public domain | W3C validator |