![]() |
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 6364 | . 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1522 ⟶wf 6221 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-fn 6228 df-f 6229 |
This theorem is referenced by: fresaun 6417 fmpox 7621 fmpo 7622 tposf 7771 issmo 7837 axdc3lem4 9721 cardf 9818 smobeth 9854 seqf2 13239 hashfxnn0 13547 snopiswrd 13716 iswrddm0 13734 s1dm 13806 s2dm 14088 ntrivcvgtail 15089 vdwlem8 16153 0ram 16185 gsumws1 17815 ga0 18169 efgsp1 18590 efgsfo 18592 efgredleme 18596 efgred 18601 ablfaclem2 18925 islinds2 20639 pmatcollpw3fi1lem1 21078 0met 22659 dvef 24260 dvfsumrlim2 24312 dchrisum0 25778 trgcgrg 25983 tgcgr4 25999 axlowdimlem4 26414 uhgr0e 26539 vtxdumgrval 26951 wlkp1 27148 pthdlem2 27236 0wlk 27582 0spth 27592 0clwlkv 27597 wlk2v2e 27623 wlkl0 27838 padct 30143 mbfmcnt 31143 coinfliprv 31357 noxp1o 32779 matunitlindf 34421 fdc 34552 grposnOLD 34692 rabren3dioph 38897 amgm2d 40037 amgm3d 40038 fco3 41031 fourierdlem80 42013 sge0iun 42243 0ome 42353 issmflem 42546 2ffzoeq 43044 nnsum4primesodd 43443 nnsum4primesoddALTV 43444 nnsum4primeseven 43447 nnsum4primesevenALTV 43448 line2x 44222 line2y 44223 amgmw2d 44385 |
Copyright terms: Public domain | W3C validator |