![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1oeq1 | GIF version |
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1oeq1 | ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq1 5224 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) | |
2 | foeq1 5242 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵)) | |
3 | 1, 2 | anbi12d 458 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))) |
4 | df-f1o 5035 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) | |
5 | df-f1o 5035 | . 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 222 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1290 –1-1→wf1 5025 –onto→wfo 5026 –1-1-onto→wf1o 5027 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-v 2622 df-un 3004 df-in 3006 df-ss 3013 df-sn 3456 df-pr 3457 df-op 3459 df-br 3852 df-opab 3906 df-rel 4459 df-cnv 4460 df-co 4461 df-dm 4462 df-rn 4463 df-fun 5030 df-fn 5031 df-f 5032 df-f1 5033 df-fo 5034 df-f1o 5035 |
This theorem is referenced by: f1oeq123d 5263 f1ocnvb 5280 f1orescnv 5282 f1ovi 5305 f1osng 5307 f1oresrab 5477 fsn 5483 isoeq1 5594 mapsn 6461 mapsnf1o3 6468 f1oen3g 6525 ensn1 6567 xpcomf1o 6595 xpen 6615 seq3f1olemstep 9991 seq3f1olemp 9992 fihasheqf1oi 10257 fihashf1rn 10258 hashfacen 10302 isummo 10834 fisum 10839 |
Copyright terms: Public domain | W3C validator |