Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1oeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1oeq2 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq2 6097 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | |
2 | foeq2 6112 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) | |
3 | 1, 2 | anbi12d 747 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))) |
4 | df-f1o 5895 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶)) | |
5 | df-f1o 5895 | . 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 384 = wceq 1483 –1-1→wf1 5885 –onto→wfo 5886 –1-1-onto→wf1o 5887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 |
This theorem is referenced by: f1oeq23 6130 f1oeq123d 6133 resin 6158 f1osng 6177 f1o2sn 6408 fveqf1o 6557 isoeq4 6570 oacomf1o 7645 bren 7964 f1dmvrnfibi 8250 marypha1lem 8339 oef1o 8595 cnfcomlem 8596 cnfcom 8597 cnfcom2 8599 infxpenc 8841 infxpenc2 8845 pwfseqlem5 9485 pwfseq 9486 summolem3 14445 summo 14448 fsum 14451 fsumf1o 14454 sumsnf 14473 sumsn 14475 prodmolem3 14663 prodmo 14666 fprod 14671 fprodf1o 14676 prodsn 14692 prodsnf 14694 gsumvalx 17270 gsumpropd 17272 gsumpropd2lem 17273 gsumval3lem1 18306 gsumval3 18308 znhash 19907 znunithash 19913 imasf1oxms 22294 cncfcnvcn 22724 wlksnwwlknvbij 26803 clwwlksvbij 26922 eupthp1 27076 f1ocnt 29559 derangval 31149 subfacp1lem2a 31162 subfacp1lem3 31164 subfacp1lem5 31166 erdsze2lem1 31185 ismtyval 33599 rngoisoval 33776 lautset 35368 pautsetN 35384 eldioph2lem1 37323 imasgim 37670 sumsnd 39185 f1oeq2d 39361 stoweidlem35 40252 stoweidlem39 40256 uspgrsprfo 41756 |
Copyright terms: Public domain | W3C validator |