![]() |
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 6372 | . 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 198 = wceq 1656 –1-1-onto→wf1o 6126 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-cleq 2818 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 |
This theorem is referenced by: f1osng 6422 f1o2sn 6663 fveqf1o 6817 oacomf1o 7917 marypha1lem 8614 oef1o 8879 cnfcomlem 8880 cnfcom2 8883 infxpenc 9161 pwfseqlem5 9807 pwfseq 9808 summolem3 14829 summo 14832 fsum 14835 prodmolem3 15043 prodmo 15046 fprod 15051 gsumvalx 17630 gsumpropd 17632 gsumpropd2lem 17633 gsumval3lem1 18666 gsumval3 18668 cncfcnvcn 23101 isismt 25853 f1ocnt 30102 erdsze2lem1 31727 ismtyval 34136 rngoisoval 34313 lautset 36152 pautsetN 36168 eldioph2lem1 38162 imasgim 38508 stoweidlem35 41040 stoweidlem39 41044 isomgreqve 42557 |
Copyright terms: Public domain | W3C validator |