![]() |
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 6736 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵)) | |
2 | foeq3 6755 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))) |
4 | df-f1o 6504 | . 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴)) | |
5 | df-f1o 6504 | . 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 205 ∧ wa 397 = wceq 1542 –1-1→wf1 6494 –onto→wfo 6495 –1-1-onto→wf1o 6496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-in 3918 df-ss 3928 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 |
This theorem is referenced by: f1oeq23 6776 f1oeq123d 6779 f1oeq3d 6782 f1ores 6799 resin 6807 isoeq5 7267 breng 8893 brenOLD 8895 xpcomf1o 9006 isinf 9205 isinfOLD 9206 cnfcom2 9639 fin1a2lem6 10342 pwfseqlem5 10600 pwfseq 10601 hashgf1o 13877 axdc4uzlem 13889 sumeq1 15574 prodeq1f 15792 unbenlem 16781 4sqlem11 16828 gsumvalx 18532 cayley 19197 cayleyth 19198 ovolicc2lem4 24887 logf1o2 26008 uspgrf1oedg 28127 wlkiswwlks2lem4 28820 clwwlknonclwlknonf1o 29309 dlwwlknondlwlknonf1o 29312 adjbd1o 31030 rinvf1o 31547 cshf1o 31819 eulerpartgbij 32975 eulerpartlemgh 32981 derangval 33764 subfacp1lem2a 33777 subfacp1lem3 33779 subfacp1lem5 33781 mrsubff1o 34112 msubff1o 34154 bj-finsumval0 35759 f1omptsnlem 35810 f1omptsn 35811 poimirlem9 36090 poimirlem15 36096 ismtyval 36262 ismrer1 36300 lautset 38548 pautsetN 38564 hvmap1o2 40231 pwfi2f1o 41426 imasgim 41430 alephiso2 41837 f1ocof1ob2 45321 isomushgr 46025 uspgrsprfo 46057 |
Copyright terms: Public domain | W3C validator |