| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1oeq2d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| Ref | Expression |
|---|---|
| f1oeq2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| f1oeq2d | ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1oeq2d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | f1oeq2 6837 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 –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: f1osng 6889 f1o2sn 7162 fveqf1o 7322 oacomf1o 8603 marypha1lem 9473 oef1o 9738 cnfcomlem 9739 cnfcom2 9742 infxpenc 10058 pwfseqlem5 10703 pwfseq 10704 summolem3 15750 summo 15753 fsum 15756 prodmolem3 15969 prodmo 15972 fprod 15977 gsumvalx 18689 gsumpropd 18691 gsumpropd2lem 18692 gsumval3lem1 19923 gsumval3 19925 cncfcnvcn 24952 isismt 28542 f1ocnt 32804 erdsze2lem1 35208 ismtyval 37807 rngoisoval 37984 lautset 40084 pautsetN 40100 sticksstones3 42149 sticksstones20 42167 eldioph2lem1 42771 imasgim 43112 stoweidlem35 46050 stoweidlem39 46054 3f1oss1 47087 isubgr3stgrlem1 47933 isubgr3stgr 47942 |
| Copyright terms: Public domain | W3C validator |