Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1oeq3d | Structured version Visualization version GIF version |
Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
f1oeq3d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
f1oeq3d | ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq3d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | f1oeq3 6600 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 –1-1-onto→wf1o 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3942 df-ss 3951 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 |
This theorem is referenced by: resdif 6629 f1osng 6649 f1oresrab 6882 fveqf1o 7049 isoini2 7081 oacomf1o 8181 mapsnf1o 8492 domss2 8665 wemapwe 9149 oef1o 9150 cnfcomlem 9151 cnfcom3 9156 cnfcom3clem 9157 infxpenc 9433 infxpenc2lem1 9434 infxpenc2 9437 ackbij2lem2 9651 hsmexlem1 9837 fsumss 15072 fsumcnv 15118 fprodss 15292 fprodcnv 15327 pwssnf1o 16761 catcisolem 17356 equivestrcsetc 17392 yoniso 17525 gsumpropd 17878 gsumpropd2lem 17879 xpsmnd 17941 xpsgrp 18158 gsumval3lem1 18956 gsumval3lem2 18957 gsumcom2 19026 coe1mul2lem2 20366 scmatrngiso 21075 m2cpmrngiso 21296 cncfcnvcn 23458 isismt 26248 usgrf1oedg 26917 wlkiswwlks2lem5 27579 clwwlkvbij 27820 eupthres 27922 eupthp1 27923 cycpmconjvlem 30711 tocyccntz 30714 dimkerim 30923 poimirlem9 34783 rngoisoval 35138 frlmsnic 39029 sge0f1o 42545 nnfoctbdj 42619 f1oresf1o 43370 ushrisomgr 43853 |
Copyright terms: Public domain | W3C validator |