![]() |
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 6698 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1540 ⟶wf 6539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-fun 6545 df-fn 6546 df-f 6547 |
This theorem is referenced by: ftpg 7156 fpropnf1 7269 suppsnop 8168 seqomlem2 8457 addnqf 10949 mulnqf 10950 isumsup2 15799 ruclem6 16185 sadcf 16401 sadadd2lem 16407 sadadd3 16409 sadaddlem 16414 smupf 16426 algrf 16517 funcoppc 17832 pmtr3ncomlem1 19386 znf1o 21330 ovolfsf 25233 ovolsf 25234 ovoliunlem1 25264 ovoliun 25267 ovoliun2 25268 voliunlem3 25314 itgss3 25577 dvexp 25718 efcn 26206 gamf 26798 basellem9 26844 axlowdimlem10 28491 wlkres 29209 1wlkdlem1 29672 vsfval 30168 ho0f 31286 opsqrlem4 31678 pjinvari 31726 fmptdF 32163 omssubaddlem 33611 omssubadd 33612 sitgclg 33654 sitgaddlemb 33660 coinfliprv 33794 plymul02 33870 signshf 33912 circum 34972 knoppcnlem8 35692 knoppcnlem11 35695 poimirlem31 36835 diophren 41866 clsf2 43192 seff 43383 binomcxplemnotnn0 43430 volicoff 45022 fourierdlem62 45195 fourierdlem80 45213 fourierdlem97 45230 carageniuncllem2 45549 0ome 45556 fcoresf1 46090 fcoresfo 46092 fundcmpsurinjimaid 46390 lindslinindimp2lem2 47240 zlmodzxzldeplem1 47281 line2 47538 |
Copyright terms: Public domain | W3C validator |