![]() |
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 6709 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ⟶wf 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2720 df-fn 6556 df-f 6557 |
This theorem is referenced by: fco3OLD 6762 fresaun 6773 fmpox 8077 fmpo 8078 tposf 8266 issmo 8375 axdc3lem4 10484 cardf 10581 smobeth 10617 seqf2 14026 hashfxnn0 14336 snopiswrd 14513 iswrddm0 14528 s1dm 14598 s2dm 14881 ntrivcvgtail 15886 vdwlem8 16964 0ram 16996 gsumws1 18797 ga0 19256 efgsp1 19699 efgsfo 19701 efgredleme 19705 efgred 19710 ablfaclem2 20050 islinds2 21754 pmatcollpw3fi1lem1 22708 0met 24292 dvef 25932 dvfsumrlim2 25987 dchrisum0 27473 noxp1o 27616 trgcgrg 28339 tgcgr4 28355 axlowdimlem4 28776 uhgr0e 28904 vtxdumgrval 29320 wlkp1 29515 pthdlem2 29602 0wlk 29946 0spth 29956 0clwlkv 29961 wlk2v2e 29987 wlkl0 30197 padct 32522 mbfmcnt 33921 coinfliprv 34135 matunitlindf 37124 fdc 37251 grposnOLD 37388 rabren3dioph 42266 amgm2d 43659 amgm3d 43660 fourierdlem80 45603 sge0iun 45836 0ome 45946 issmflem 46144 2ffzoeq 46737 nnsum4primesodd 47165 nnsum4primesoddALTV 47166 nnsum4primeseven 47169 nnsum4primesevenALTV 47170 line2x 47905 line2y 47906 amgmw2d 48315 |
Copyright terms: Public domain | W3C validator |