|   | 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 6715 | . 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 ⟶wf 6556 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-br 5143 df-opab 5205 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-fun 6562 df-fn 6563 df-f 6564 | 
| This theorem is referenced by: ftpg 7175 fpropnf1 7288 suppsnop 8204 seqomlem2 8492 addnqf 10989 mulnqf 10990 isumsup2 15883 ruclem6 16272 sadcf 16491 sadadd2lem 16497 sadadd3 16499 sadaddlem 16504 smupf 16516 algrf 16611 funcoppc 17921 pmtr3ncomlem1 19492 znf1o 21571 ovolfsf 25507 ovolsf 25508 ovoliunlem1 25538 ovoliun 25541 ovoliun2 25542 voliunlem3 25588 itgss3 25851 dvexp 25992 efcn 26488 gamf 27087 basellem9 27133 axlowdimlem10 28967 wlkres 29689 1wlkdlem1 30157 vsfval 30653 ho0f 31771 opsqrlem4 32163 pjinvari 32211 fmptdF 32667 omssubaddlem 34302 omssubadd 34303 sitgclg 34345 sitgaddlemb 34351 coinfliprv 34486 plymul02 34562 signshf 34604 circum 35680 knoppcnlem8 36502 knoppcnlem11 36505 poimirlem31 37659 diophren 42829 clsf2 44144 seff 44333 binomcxplemnotnn0 44380 volicoff 46015 fourierdlem62 46188 fourierdlem80 46206 fourierdlem97 46223 carageniuncllem2 46542 0ome 46549 fcoresf1 47086 fcoresfo 47088 fundcmpsurinjimaid 47403 isubgruhgr 47859 lindslinindimp2lem2 48381 zlmodzxzldeplem1 48422 line2 48678 | 
| Copyright terms: Public domain | W3C validator |