![]() |
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 6735 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | |
2 | foeq2 6754 | . . 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-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2729 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 |
This theorem is referenced by: f1oeq23 6776 f1oeq123d 6779 f1oeq2d 6781 resin 6807 isoeq4 7266 breng 8893 brenOLD 8895 f1dmvrnfibi 9281 cnfcom 9637 infxpenc2 9959 fsumf1o 15609 sumsnf 15629 fprodf1o 15830 prodsn 15846 prodsnf 15848 znhash 20968 znunithash 20974 imasf1oxms 23848 wlksnwwlknvbij 28856 clwwlkvbij 29060 eupthp1 29163 derangval 33764 subfacp1lem2a 33777 subfacp1lem3 33779 subfacp1lem5 33781 sumsnd 43238 uspgrsprfo 46057 |
Copyright terms: Public domain | W3C validator |