MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funmpt Structured version   Visualization version   GIF version

Theorem funmpt 6108
Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
Assertion
Ref Expression
funmpt Fun (𝑥𝐴𝐵)

Proof of Theorem funmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 funopab4 6107 . 2 Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
2 df-mpt 4891 . . 3 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
32funeqi 6091 . 2 (Fun (𝑥𝐴𝐵) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)})
41, 3mpbir 222 1 Fun (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1652  wcel 2155  {copab 4873  cmpt 4890  Fun wfun 6064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-fun 6072
This theorem is referenced by:  funmpt2  6109  resfunexg  6674  mptexg  6679  mptexgf  6680  brtpos2  7563  tposfun  7573  mptfi  8474  sniffsupp  8524  cantnfrescl  8790  cantnflem1  8803  r0weon  9088  axcc2lem  9513  mptct  9615  negfi  11227  mptnn0fsupp  13007  ccatalpha  13567  mreacs  16587  acsfn  16588  isofval  16685  lubfun  17249  glbfun  17262  acsficl2d  17445  pmtrsn  18206  gsum2dlem2  18639  gsum2d  18640  dprdfinv  18688  dprdfadd  18689  dmdprdsplitlem  18706  dpjidcl  18727  mptscmfsupp0  19200  00lsp  19256  psrass1lem  19654  psrlidm  19680  psrridm  19681  psrass1  19682  psrass23l  19685  psrcom  19686  psrass23  19687  mplsubrg  19717  mplmon  19740  mplmonmul  19741  mplcoe1  19742  mplcoe5  19745  mplbas2  19747  evlslem2  19788  evlslem6  19789  psropprmul  19884  coe1mul2  19915  pjpm  20331  frlmphllem  20398  frlmphl  20399  uvcff  20409  uvcresum  20411  oftpos  20538  pmatcollpw2lem  20864  tgrest  21246  cmpfi  21494  1stcrestlem  21538  ptcnplem  21707  xkoinjcn  21773  symgtgp  22187  eltsms  22218  cphsscph  23331  rrxmval  23480  tdeglem4  24114  plypf1  24262  tayl0  24410  taylthlem1  24421  xrlimcnp  24989  abrexexd  29799  fmptcof2  29910  ofpreima  29918  mptctf  29947  psgnfzto1stlem  30300  locfinreflem  30357  measdivcstOLD  30737  sxbrsigalem0  30783  sitgf  30859  nosupno  32296  imageval  32484  poimirlem30  33866  poimir  33869  choicefi  40040  fourierdlem80  41043  sge0tsms  41237  scmsuppss  42825  rmfsupp  42827  scmfsupp  42831  fdivval  43005
  Copyright terms: Public domain W3C validator