| 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 6717 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fn 6564 df-f 6565 |
| This theorem is referenced by: fresaun 6779 fmpox 8092 fmpo 8093 tposf 8279 issmo 8388 axdc3lem4 10493 cardf 10590 smobeth 10626 seqf2 14062 hashfxnn0 14376 snopiswrd 14561 iswrddm0 14576 s1dm 14646 s2dm 14929 s7f1o 15005 ntrivcvgtail 15936 vdwlem8 17026 0ram 17058 gsumws1 18851 ga0 19316 efgsp1 19755 efgsfo 19757 efgredleme 19761 efgred 19766 ablfaclem2 20106 islinds2 21833 rhmply1vsca 22392 pmatcollpw3fi1lem1 22792 0met 24376 dvef 26018 dvfsumrlim2 26073 dchrisum0 27564 noxp1o 27708 trgcgrg 28523 tgcgr4 28539 axlowdimlem4 28960 uhgr0e 29088 vtxdumgrval 29504 wlkp1 29699 pthdlem2 29788 0wlk 30135 0spth 30145 0clwlkv 30150 wlk2v2e 30176 wlkl0 30386 padct 32731 wrdpmtrlast 33113 mbfmcnt 34270 coinfliprv 34485 matunitlindf 37625 fdc 37752 grposnOLD 37889 rabren3dioph 42826 amgm2d 44211 amgm3d 44212 fourierdlem80 46201 sge0iun 46434 0ome 46544 issmflem 46742 2ffzoeq 47339 nnsum4primesodd 47783 nnsum4primesoddALTV 47784 nnsum4primeseven 47787 nnsum4primesevenALTV 47788 line2x 48675 line2y 48676 amgmw2d 49323 |
| Copyright terms: Public domain | W3C validator |