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

Theorem funmpt 6075
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 6074 . 2 Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
2 df-mpt 4870 . . 3 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
32funeqi 6058 . 2 (Fun (𝑥𝐴𝐵) ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)})
41, 3mpbir 221 1 Fun (𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1620  wcel 2127  {copab 4852  cmpt 4869  Fun wfun 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-fun 6039
This theorem is referenced by:  funmpt2  6076  resfunexg  6631  mptexg  6636  mptexgf  6637  brtpos2  7515  tposfun  7525  mptfi  8418  sniffsupp  8468  cantnfrescl  8734  cantnflem1  8747  r0weon  8996  axcc2lem  9421  mptct  9523  negfi  11134  mptnn0fsupp  12962  ccatalpha  13536  mreacs  16491  acsfn  16492  isofval  16589  lubfun  17152  glbfun  17165  acsficl2d  17348  pmtrsn  18110  gsum2dlem2  18541  gsum2d  18542  dprdfinv  18589  dprdfadd  18590  dmdprdsplitlem  18607  dpjidcl  18628  mptscmfsupp0  19101  00lsp  19154  psrass1lem  19550  psrlidm  19576  psrridm  19577  psrass1  19578  psrass23l  19581  psrcom  19582  psrass23  19583  mplsubrg  19613  mplmon  19636  mplmonmul  19637  mplcoe1  19638  mplcoe5  19641  mplbas2  19643  evlslem2  19685  evlslem6  19686  psropprmul  19781  coe1mul2  19812  pjpm  20225  frlmphllem  20292  frlmphl  20293  uvcff  20303  uvcresum  20305  oftpos  20431  pmatcollpw2lem  20755  tgrest  21136  cmpfi  21384  1stcrestlem  21428  ptcnplem  21597  xkoinjcn  21663  symgtgp  22077  eltsms  22108  rrxmval  23359  tdeglem4  23990  plypf1  24138  tayl0  24286  taylthlem1  24297  xrlimcnp  24865  abrexexd  29625  fmptcof2  29737  ofpreima  29745  funcnvmptOLD  29747  mptctf  29775  psgnfzto1stlem  30130  locfinreflem  30187  measdivcstOLD  30567  sxbrsigalem0  30613  sitgf  30689  nosupno  32126  imageval  32314  poimirlem30  33721  poimir  33724  choicefi  39860  fourierdlem80  40875  sge0tsms  41069  scmsuppss  42632  rmfsupp  42634  scmfsupp  42638  fdivval  42812
  Copyright terms: Public domain W3C validator