![]() |
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 6822 | . 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 1542 –1-1-onto→wf1o 6543 |
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-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 |
This theorem is referenced by: f1orescnv 6849 f1osng 6875 f1ofvswap 7304 dif1en 9160 dif1enOLD 9162 cnfcomlem 9694 cnfcom2 9697 cnfcom3clem 9700 infxpenc 10013 infxpenc2lem2 10015 infxpenc2 10017 canthp1lem2 10648 pwfseqlem5 10658 pwfseq 10659 s2f1o 14867 s4f1o 14869 bitsf1ocnv 16385 yonffthlem 18235 grplactcnv 18926 eqgen 19061 znunithash 21120 tgpconncompeqg 23616 fcobijfs 31948 s2f1 32111 mgcf1o 32173 gsummpt2d 32201 indf1o 33022 subfacp1lem3 34173 subfacp1lem5 34175 ismrer1 36706 hvmap1o 40634 metakunt34 41018 |
Copyright terms: Public domain | W3C validator |