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 6490 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1533 ⟶wf 6346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-fun 6352 df-fn 6353 df-f 6354 |
This theorem is referenced by: ftpg 6913 fpropnf1 7019 suppsnop 7838 seqomlem2 8081 addnqf 10364 mulnqf 10365 isumsup2 15195 ruclem6 15582 sadcf 15796 sadadd2lem 15802 sadadd3 15804 sadaddlem 15809 smupf 15821 algrf 15911 funcoppc 17139 pmtr3ncomlem1 18595 znf1o 20692 ovolfsf 24066 ovolsf 24067 ovoliunlem1 24097 ovoliun 24100 ovoliun2 24101 voliunlem3 24147 itgss3 24409 dvexp 24544 efcn 25025 gamf 25614 basellem9 25660 axlowdimlem10 26731 wlkres 27446 1wlkdlem1 27910 vsfval 28404 ho0f 29522 opsqrlem4 29914 pjinvari 29962 fmptdF 30395 omssubaddlem 31552 omssubadd 31553 sitgclg 31595 sitgaddlemb 31601 coinfliprv 31735 plymul02 31811 signshf 31853 circum 32912 knoppcnlem8 33834 knoppcnlem11 33837 poimirlem31 34917 diophren 39403 clsf2 40469 seff 40634 binomcxplemnotnn0 40681 volicoff 42273 fourierdlem62 42446 fourierdlem80 42464 fourierdlem97 42481 carageniuncllem2 42797 0ome 42804 fundcmpsurinjimaid 43564 mapprop 44387 lindslinindimp2lem2 44507 zlmodzxzldeplem1 44548 line2 44732 |
Copyright terms: Public domain | W3C validator |