![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feq1i | Structured version Visualization version GIF version |
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
feq1i.1 | ⊢ 𝐹 = 𝐺 |
Ref | Expression |
---|---|
feq1i | ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq1i.1 | . 2 ⊢ 𝐹 = 𝐺 | |
2 | feq1 6325 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1507 ⟶wf 6184 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-fun 6190 df-fn 6191 df-f 6192 |
This theorem is referenced by: ftpg 6741 fpropnf1 6850 suppsnop 7647 seqomlem2 7890 addnqf 10168 mulnqf 10169 isumsup2 15061 ruclem6 15448 sadcf 15662 sadadd2lem 15668 sadadd3 15670 sadaddlem 15675 smupf 15687 algrf 15773 funcoppc 17003 pmtr3ncomlem1 18362 znf1o 20400 ovolfsf 23775 ovolsf 23776 ovoliunlem1 23806 ovoliun 23809 ovoliun2 23810 voliunlem3 23856 itgss3 24118 dvexp 24253 efcn 24734 gamf 25322 basellem9 25368 axlowdimlem10 26440 wlkres 27156 wlkresOLD 27158 1wlkdlem1 27666 vsfval 28187 ho0f 29309 opsqrlem4 29701 pjinvari 29749 fmptdF 30163 omssubaddlem 31208 omssubadd 31209 sitgclg 31251 sitgaddlemb 31257 coinfliprv 31392 plymul02 31468 signshf 31512 circum 32443 knoppcnlem8 33365 knoppcnlem11 33368 poimirlem31 34370 diophren 38812 clsf2 39845 seff 40063 binomcxplemnotnn0 40110 volicoff 41717 fourierdlem62 41890 fourierdlem80 41908 fourierdlem97 41925 carageniuncllem2 42241 0ome 42248 mapprop 43764 lindslinindimp2lem2 43887 zlmodzxzldeplem1 43928 line2 44113 |
Copyright terms: Public domain | W3C validator |