| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > f1oeq2 | GIF version | ||
| Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
| Ref | Expression |
|---|---|
| f1oeq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1eq2 5476 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | |
| 2 | foeq2 5494 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) | |
| 3 | 1, 2 | anbi12d 473 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))) |
| 4 | df-f1o 5277 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶)) | |
| 5 | df-f1o 5277 | . 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)) | |
| 6 | 3, 4, 5 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1372 –1-1→wf1 5267 –onto→wfo 5268 –1-1-onto→wf1o 5269 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1469 ax-gen 1471 ax-4 1532 ax-17 1548 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 df-fn 5273 df-f 5274 df-f1 5275 df-fo 5276 df-f1o 5277 |
| This theorem is referenced by: f1oeq23 5512 f1oeq123d 5515 f1oeq2d 5517 f1osng 5562 isoeq4 5872 breng 6833 bren 6834 f1dmvrnfibi 7045 summodclem3 11662 summodclem2a 11663 summodc 11665 fsum3 11669 fsumf1o 11672 sumsnf 11691 fprodf1o 11870 prodsnf 11874 znfi 14388 znhash 14389 |
| Copyright terms: Public domain | W3C validator |