Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > feq2i | Structured version Visualization version GIF version |
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.) |
Ref | Expression |
---|---|
feq2i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
feq2i | ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq2i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | feq2 6490 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ⟶wf 6345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-fn 6352 df-f 6353 |
This theorem is referenced by: fresaun 6543 fmpox 7756 fmpo 7757 tposf 7911 issmo 7976 axdc3lem4 9864 cardf 9961 smobeth 9997 seqf2 13379 hashfxnn0 13687 snopiswrd 13860 iswrddm0 13878 s1dm 13952 s2dm 14242 ntrivcvgtail 15246 vdwlem8 16314 0ram 16346 gsumws1 17992 ga0 18368 efgsp1 18794 efgsfo 18796 efgredleme 18800 efgred 18805 ablfaclem2 19139 islinds2 20887 pmatcollpw3fi1lem1 21324 0met 22905 dvef 24506 dvfsumrlim2 24558 dchrisum0 26024 trgcgrg 26229 tgcgr4 26245 axlowdimlem4 26659 uhgr0e 26784 vtxdumgrval 27196 wlkp1 27391 pthdlem2 27477 0wlk 27823 0spth 27833 0clwlkv 27838 wlk2v2e 27864 wlkl0 28074 padct 30382 mbfmcnt 31426 coinfliprv 31640 noxp1o 33068 matunitlindf 34772 fdc 34903 grposnOLD 35043 rabren3dioph 39292 amgm2d 40432 amgm3d 40433 fco3 41371 fourierdlem80 42352 sge0iun 42582 0ome 42692 issmflem 42885 2ffzoeq 43409 nnsum4primesodd 43808 nnsum4primesoddALTV 43809 nnsum4primeseven 43812 nnsum4primesevenALTV 43813 line2x 44639 line2y 44640 amgmw2d 44803 |
Copyright terms: Public domain | W3C validator |