![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
f1oeq1d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
Ref | Expression |
---|---|
f1oeq1d | ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq1d.1 | . 2 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | f1oeq1 6830 | . 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 6550 |
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-8 2100 ax-9 2108 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151 df-opab 5213 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-rn 5691 df-fun 6553 df-fn 6554 df-f 6555 df-f1 6556 df-fo 6557 df-f1o 6558 |
This theorem is referenced by: f1orescnv 6857 f1osng 6883 f1ofvswap 7319 dif1en 9189 dif1enOLD 9191 cnfcomlem 9728 cnfcom2 9731 cnfcom3clem 9734 infxpenc 10047 infxpenc2lem2 10049 infxpenc2 10051 canthp1lem2 10682 pwfseqlem5 10692 pwfseq 10693 s2f1o 14905 s4f1o 14907 bitsf1ocnv 16424 yonffthlem 18279 grplactcnv 19004 eqgen 19141 znunithash 21503 tgpconncompeqg 24034 fcobijfs 32523 s2f1 32686 mgcf1o 32748 gsummpt2d 32781 indf1o 33648 subfacp1lem3 34797 subfacp1lem5 34799 ismrer1 37316 hvmap1o 41240 metakunt34 41694 |
Copyright terms: Public domain | W3C validator |