![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oeq3 | Structured version Visualization version GIF version |
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1oeq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq3 6136 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵)) | |
2 | foeq3 6151 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) | |
3 | 1, 2 | anbi12d 747 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))) |
4 | df-f1o 5933 | . 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴)) | |
5 | df-f1o 5933 | . 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 –1-1→wf1 5923 –onto→wfo 5924 –1-1-onto→wf1o 5925 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 |
This theorem is referenced by: f1oeq23 6168 f1oeq123d 6171 f1oeq3d 6172 f1ores 6189 resin 6196 f1osng 6215 f1oresrab 6435 fveqf1o 6597 isoeq5 6611 isoini2 6629 ncanth 6649 oacomf1o 7690 mapsnf1o 7991 bren 8006 xpcomf1o 8090 domss2 8160 isinf 8214 wemapwe 8632 oef1o 8633 cnfcomlem 8634 cnfcom2 8637 cnfcom3 8639 cnfcom3clem 8640 infxpenc 8879 infxpenc2lem1 8880 infxpenc2 8883 fin1a2lem6 9265 hsmexlem1 9286 pwfseqlem5 9523 pwfseq 9524 hashgf1o 12810 axdc4uzlem 12822 sumeq1 14463 fsumss 14500 fsumcnv 14548 prodeq1f 14682 fprodss 14722 fprodcnv 14757 unbenlem 15659 4sqlem11 15706 pwssnf1o 16205 catcisolem 16803 yoniso 16972 gsumvalx 17317 gsumpropd 17319 gsumpropd2lem 17320 xpsmnd 17377 xpsgrp 17581 cayley 17880 cayleyth 17881 gsumval3lem1 18352 gsumval3lem2 18353 gsumcom2 18420 scmatrngiso 20390 m2cpmrngiso 20611 cncfcnvcn 22771 ovolicc2lem4 23334 logf1o2 24441 uspgrf1oedg 26113 wlkiswwlks2lem4 26826 clwwlkvbijOLD 27089 adjbd1o 29072 rinvf1o 29560 eulerpartgbij 30562 eulerpartlemgh 30568 derangval 31275 subfacp1lem2a 31288 subfacp1lem3 31290 subfacp1lem5 31292 mrsubff1o 31538 msubff1o 31580 bj-finsumval0 33277 f1omptsnlem 33313 f1omptsn 33314 poimirlem4 33543 poimirlem9 33548 poimirlem15 33554 ismtyval 33729 ismrer1 33767 rngoisoval 33906 lautset 35686 pautsetN 35702 hvmap1o2 37371 pwfi2f1o 37983 imasgim 37987 uspgrsprfo 42081 |
Copyright terms: Public domain | W3C validator |