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 6489 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ⟶wf 6344 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-fn 6351 df-f 6352 |
This theorem is referenced by: fresaun 6542 fmpox 7754 fmpo 7755 tposf 7909 issmo 7974 axdc3lem4 9863 cardf 9960 smobeth 9996 seqf2 13377 hashfxnn0 13685 snopiswrd 13858 iswrddm0 13876 s1dm 13950 s2dm 14240 ntrivcvgtail 15244 vdwlem8 16312 0ram 16344 gsumws1 17990 ga0 18366 efgsp1 18792 efgsfo 18794 efgredleme 18798 efgred 18803 ablfaclem2 19137 islinds2 20885 pmatcollpw3fi1lem1 21322 0met 22903 dvef 24504 dvfsumrlim2 24556 dchrisum0 26023 trgcgrg 26228 tgcgr4 26244 axlowdimlem4 26658 uhgr0e 26783 vtxdumgrval 27195 wlkp1 27390 pthdlem2 27476 0wlk 27822 0spth 27832 0clwlkv 27837 wlk2v2e 27863 wlkl0 28073 padct 30381 mbfmcnt 31425 coinfliprv 31639 noxp1o 33067 matunitlindf 34771 fdc 34901 grposnOLD 35041 rabren3dioph 39290 amgm2d 40429 amgm3d 40430 fco3 41367 fourierdlem80 42348 sge0iun 42578 0ome 42688 issmflem 42881 2ffzoeq 43405 nnsum4primesodd 43838 nnsum4primesoddALTV 43839 nnsum4primeseven 43842 nnsum4primesevenALTV 43843 line2x 44669 line2y 44670 amgmw2d 44833 |
Copyright terms: Public domain | W3C validator |