![]() |
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 6834 | . 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 205 = wceq 1533 –1-1-onto→wf1o 6552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-in 3956 df-ss 3966 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 |
This theorem is referenced by: resdif 6865 f1osng 6885 f1oresrab 7142 fveqf1o 7318 isoini2 7353 oacomf1o 8592 mapsnf1o 8964 domss2 9167 dif1enlem 9187 dif1enlemOLD 9188 infn0 9338 wemapwe 9728 oef1o 9729 cnfcomlem 9730 cnfcom3 9735 cnfcom3clem 9736 infxpenc 10049 infxpenc2lem1 10050 infxpenc2 10053 ackbij2lem2 10271 hsmexlem1 10457 fsumss 15711 fsumcnv 15759 fprodss 15932 fprodcnv 15967 pwssnf1o 17487 catcisolem 18106 equivestrcsetc 18150 yoniso 18284 gsumpropd 18645 gsumpropd2lem 18646 xpsmnd 18741 xpsgrp 19022 ghmqusker 19245 gsumval3lem1 19867 gsumval3lem2 19868 gsumcom2 19937 xpsrngd 20126 xpsringd 20275 rngqiprngim 21201 coe1mul2lem2 22194 scmatrngiso 22458 m2cpmrngiso 22680 cncfcnvcn 24866 isismt 28358 usgrf1oedg 29040 wlkiswwlks2lem5 29704 clwwlkvbij 29943 eupthres 30045 eupthp1 30046 cycpmconjvlem 32883 tocyccntz 32886 idomsubr 33020 dimkerim 33358 poimirlem4 37130 poimirlem9 37135 rngoisoval 37483 frlmsnic 41801 sge0f1o 45799 nnfoctbdj 45873 f1oresf1o 46699 grimidvtxedg 47252 ushggricedg 47271 |
Copyright terms: Public domain | W3C validator |