![]() |
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 6801 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | |
2 | foeq2 6818 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))) |
4 | df-f1o 6570 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶)) | |
5 | df-f1o 6570 | . 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 –1-1→wf1 6560 –onto→wfo 6561 –1-1-onto→wf1o 6562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 |
This theorem is referenced by: f1oeq23 6840 f1oeq123d 6843 f1oeq2d 6845 resin 6871 isoeq4 7340 breng 8993 f1dmvrnfibi 9379 cnfcom 9738 infxpenc2 10060 fsumf1o 15756 sumsnf 15776 fprodf1o 15979 prodsn 15995 prodsnf 15997 znhash 21595 znunithash 21601 imasf1oxms 24518 wlksnwwlknvbij 29938 clwwlkvbij 30142 eupthp1 30245 derangval 35152 subfacp1lem2a 35165 subfacp1lem3 35167 subfacp1lem5 35169 sumsnd 44964 isuspgrim0lem 47809 isubgr3stgrlem1 47869 usgrexmpl1lem 47916 usgrexmpl2lem 47921 uspgrsprfo 47992 |
Copyright terms: Public domain | W3C validator |