![]() |
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 6382 | . 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 198 = wceq 1601 –1-1-onto→wf1o 6134 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-in 3798 df-ss 3805 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 |
This theorem is referenced by: resdif 6411 f1osng 6431 f1oresrab 6659 fveqf1o 6829 isoini2 6861 oacomf1o 7929 mapsnf1o 8235 domss2 8407 wemapwe 8891 oef1o 8892 cnfcomlem 8893 cnfcom3 8898 cnfcom3clem 8899 infxpenc 9174 infxpenc2lem1 9175 infxpenc2 9178 ackbij2lem2 9397 hsmexlem1 9583 fsumss 14863 fsumcnv 14909 fprodss 15081 fprodcnv 15116 pwssnf1o 16544 catcisolem 17141 equivestrcsetc 17178 yoniso 17311 coe1mul2lem2 20034 usgrf1oedg 26553 wlkiswwlks2lem5 27222 clwwlkvbij 27515 clwwlkvbijOLD 27516 eupthresOLD 27618 eupthres 27619 eupthp1 27620 dimkerim 30441 poimirlem9 34039 sge0f1o 41516 nnfoctbdj 41590 f1oresf1o 42324 f1oresf1o2 42325 ushrisomgr 42747 |
Copyright terms: Public domain | W3C validator |