![]() |
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 6812 | . 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 205 = wceq 1533 –1-1-onto→wf1o 6532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 df-cleq 2716 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 |
This theorem is referenced by: f1osng 6864 f1o2sn 7132 fveqf1o 7293 oacomf1o 8560 marypha1lem 9423 oef1o 9688 cnfcomlem 9689 cnfcom2 9692 infxpenc 10008 pwfseqlem5 10653 pwfseq 10654 summolem3 15656 summo 15659 fsum 15662 prodmolem3 15873 prodmo 15876 fprod 15881 gsumvalx 18598 gsumpropd 18600 gsumpropd2lem 18601 gsumval3lem1 19814 gsumval3 19816 cncfcnvcn 24767 isismt 28220 f1ocnt 32448 erdsze2lem1 34649 ismtyval 37124 rngoisoval 37301 lautset 39409 pautsetN 39425 sticksstones3 41423 sticksstones20 41441 eldioph2lem1 41953 imasgim 42297 stoweidlem35 45202 stoweidlem39 45206 isomgreqve 46944 |
Copyright terms: Public domain | W3C validator |