|   | 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 6800 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | |
| 2 | foeq2 6817 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶)) | |
| 3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))) | 
| 4 | df-f1o 6568 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶)) | |
| 5 | df-f1o 6568 | . 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 1540 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 | 
| This theorem is referenced by: f1oeq23 6839 f1oeq123d 6842 f1oeq2d 6844 resin 6870 isoeq4 7340 breng 8994 f1dmvrnfibi 9381 cnfcom 9740 infxpenc2 10062 fsumf1o 15759 sumsnf 15779 fprodf1o 15982 prodsn 15998 prodsnf 16000 znhash 21577 znunithash 21583 imasf1oxms 24502 wlksnwwlknvbij 29928 clwwlkvbij 30132 eupthp1 30235 derangval 35172 subfacp1lem2a 35185 subfacp1lem3 35187 subfacp1lem5 35189 sumsnd 45031 isuspgrim0lem 47871 isubgr3stgrlem1 47933 usgrexmpl1lem 47980 usgrexmpl2lem 47985 uspgrsprfo 48064 tposf1o 48784 | 
| Copyright terms: Public domain | W3C validator |