|   | 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 6837 | . 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 206 = wceq 1539 –1-1-onto→wf1o 6559 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ss 3967 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 | 
| This theorem is referenced by: resdif 6868 f1osng 6888 f1oresrab 7146 fveqf1o 7323 isoini2 7360 oacomf1o 8604 mapsnf1o 8980 domss2 9177 dif1enlem 9197 dif1enlemOLD 9198 infn0 9341 wemapwe 9738 oef1o 9739 cnfcomlem 9740 cnfcom3 9745 cnfcom3clem 9746 infxpenc 10059 infxpenc2lem1 10060 infxpenc2 10063 ackbij2lem2 10280 hsmexlem1 10467 fsumss 15762 fsumcnv 15810 fprodss 15985 fprodcnv 16020 pwssnf1o 17544 catcisolem 18156 equivestrcsetc 18198 yoniso 18331 gsumpropd 18692 gsumpropd2lem 18693 xpsmnd 18791 xpsgrp 19078 ghmqusker 19306 gsumval3lem1 19924 gsumval3lem2 19925 gsumcom2 19994 xpsrngd 20177 xpsringd 20330 rngqiprngim 21315 coe1mul2lem2 22272 scmatrngiso 22543 m2cpmrngiso 22765 cncfcnvcn 24953 isismt 28543 usgrf1oedg 29225 wlkiswwlks2lem5 29894 clwwlkvbij 30133 eupthres 30235 eupthp1 30236 cycpmconjvlem 33162 tocyccntz 33165 idomsubr 33312 dimkerim 33679 prodeq12sdv 36220 cbvsumdavw2 36297 cbvproddavw2 36298 poimirlem4 37632 poimirlem9 37637 rngoisoval 37985 frlmsnic 42555 sge0f1o 46402 nnfoctbdj 46476 3f1oss1 47092 f1oresf1o 47307 grimidvtxedg 47881 ushggricedg 47901 uhgrimisgrgric 47904 isubgr3stgrlem3 47940 oduoppcciso 49218 | 
| Copyright terms: Public domain | W3C validator |