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

Theorem mptexg 6965
Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
mptexg (𝐴𝑉 → (𝑥𝐴𝐵) ∈ V)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem mptexg
StepHypRef Expression
1 funmpt 6366 . 2 Fun (𝑥𝐴𝐵)
2 eqid 2801 . . . 4 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
32dmmptss 6066 . . 3 dom (𝑥𝐴𝐵) ⊆ 𝐴
4 ssexg 5194 . . 3 ((dom (𝑥𝐴𝐵) ⊆ 𝐴𝐴𝑉) → dom (𝑥𝐴𝐵) ∈ V)
53, 4mpan 689 . 2 (𝐴𝑉 → dom (𝑥𝐴𝐵) ∈ V)
6 funex 6963 . 2 ((Fun (𝑥𝐴𝐵) ∧ dom (𝑥𝐴𝐵) ∈ V) → (𝑥𝐴𝐵) ∈ V)
71, 5, 6sylancr 590 1 (𝐴𝑉 → (𝑥𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444  wss 3884  cmpt 5113  dom cdm 5523  Fun wfun 6322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336
This theorem is referenced by:  mptex  6967  mptexd  6968  ovmpt3rab1  7387  offval  7400  abrexexg  7648  xpexgALT  7668  offval3  7669  suppssov1  7849  suppssfv  7853  iunon  7963  onoviun  7967  mptelixpg  8486  cantnfp1lem1  9129  updjud  9351  coftr  9688  axcc3  9853  reps  14127  wrd2f1tovbij  14319  restval  16696  resf1st  17160  resf2nd  17161  funcres  17162  vrmdfval  18017  symgfixfolem1  18562  pmtrval  18575  pmtrrn  18581  pmtrfrn  18582  sylow1lem4  18722  sylow3lem2  18749  sylow3lem3  18750  uvcfval  20477  uvcval  20478  uvcff  20484  uvcresum  20486  psrass1lem  20619  opsrval  20718  selvfval  20793  psropprmul  20871  mavmuldm  21159  mat2pmatfval  21332  cpm2mfval  21358  chpmatfval  21439  ntrfval  21633  clsfval  21634  neifval  21708  lpfval  21747  ptcnplem  22230  upxp  22232  fmfnfmlem3  22565  fmfnfmlem4  22566  ustuqtoplem  22849  ustuqtop0  22850  utopsnneiplem  22857  rrxmval  24013  tdeglem4  24665  tayl0  24961  itgulm2  25008  efabl  25146  tgjustr  26272  lmif  26583  islmib  26585  nbusgrf1o1  27164  cusgrfilem3  27251  vtxdgfval  27261  wlkiswwlks2  27665  wwlksnextbij  27692  clwlkclwwlklem1  27788  grpoinvfval  28309  acunirnmpt  30426  acunirnmpt2  30427  acunirnmpt2f  30428  aciunf1lem  30429  fnpreimac  30438  frlmdim  31101  indv  31385  indval  31386  ofcfval3  31475  omsval  31665  carsgclctunlem2  31691  pmeasadd  31697  sitgclg  31714  bnj1366  32215  ptpconn  32594  fwddifval  33737  tailfval  33834  curfv  35036  matunitlindflem1  35052  matunitlindflem2  35053  upixp  35166  pw2f1ocnv  39975  kelac1  40004  rfovd  40699  fsovrfovd  40707  dssmapfvd  40715  dssmapfv2d  40716  fmulcl  42220  fmuldfeqlem1  42221  dvnmul  42582  dvnprodlem2  42586  stoweidlem31  42670  stoweidlem42  42681  stoweidlem48  42687  etransclem1  42874  etransclem4  42877  etransclem13  42886  etransclem17  42890  0ome  43165  hoicvr  43184  hsphoif  43212  hsphoival  43215  hoidmvlelem2  43232  hoidmvlelem3  43233  ovnhoilem1  43237  ovnhoilem2  43238  ovnlecvr2  43246  ovncvr2  43247  hoidifhspval2  43251  hspmbllem2  43263  fundcmpsurinjALT  43926  sprbisymrel  44013  uspgrbisymrelALT  44380  funcrngcsetc  44619  funcringcsetc  44656  scmsuppss  44771  rmfsupp  44773  scmfsupp  44777  mptcfsupp  44779  lincresunit2  44884  itcoval0mpt  45077
  Copyright terms: Public domain W3C validator