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

Theorem mptexg 6525
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 5964 . 2 Fun (𝑥𝐴𝐵)
2 eqid 2651 . . . 4 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
32dmmptss 5669 . . 3 dom (𝑥𝐴𝐵) ⊆ 𝐴
4 ssexg 4837 . . 3 ((dom (𝑥𝐴𝐵) ⊆ 𝐴𝐴𝑉) → dom (𝑥𝐴𝐵) ∈ V)
53, 4mpan 706 . 2 (𝐴𝑉 → dom (𝑥𝐴𝐵) ∈ V)
6 funex 6523 . 2 ((Fun (𝑥𝐴𝐵) ∧ dom (𝑥𝐴𝐵) ∈ V) → (𝑥𝐴𝐵) ∈ V)
71, 5, 6sylancr 696 1 (𝐴𝑉 → (𝑥𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  Vcvv 3231  wss 3607  cmpt 4762  dom cdm 5143  Fun wfun 5920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934
This theorem is referenced by:  mptex  6527  mptexd  6528  ovmpt3rab1  6933  offval  6946  abrexexg  7182  xpexgALT  7203  offval3  7204  mptsuppdifd  7362  suppssov1  7372  suppssfv  7376  mpt2curryvald  7441  iunon  7481  onoviun  7485  mptelixpg  7987  fsuppmptif  8346  sniffsupp  8356  cantnfrescl  8611  cantnfp1lem1  8613  cantnflem1  8624  infxpenc2lem2  8881  coftr  9133  axcc3  9298  negfi  11009  seqof2  12899  reps  13563  wrd2f1tovbij  13749  ramcl  15780  restval  16134  prdsplusgval  16180  prdsmulrval  16182  prdsvscaval  16186  resf1st  16601  resf2nd  16602  funcres  16603  galactghm  17869  symgfixfolem1  17904  pmtrval  17917  pmtrrn  17923  pmtrfrn  17924  sylow1lem4  18062  sylow3lem2  18089  sylow3lem3  18090  gsum2dlem2  18416  gsum2d  18417  dprdfinv  18464  dprdfadd  18465  dmdprdsplitlem  18482  dpjfval  18500  dpjidcl  18503  mptscmfsupp0  18976  psrass1lem  19425  psrridm  19452  psrcom  19457  mvrfval  19468  mplcoe5  19516  mplbas2  19518  opsrval  19522  evlslem6  19561  psropprmul  19656  evls1sca  19736  frlmgsum  20159  frlmphllem  20167  uvcfval  20171  uvcval  20172  uvcff  20178  uvcresum  20180  matgsum  20291  mvmulval  20397  mavmuldm  20404  mavmul0g  20407  marepvval0  20420  mat2pmatfval  20576  cpm2mfval  20602  chpmatfval  20683  ntrfval  20876  clsfval  20877  neifval  20951  lpfval  20990  ptcnplem  21472  upxp  21474  xkocnv  21665  fmfnfmlem3  21807  fmfnfmlem4  21808  ptcmplem3  21905  ustuqtoplem  22090  ustuqtop0  22091  utopsnneiplem  22098  prdsdsf  22219  ressprdsds  22223  prdsxmslem2  22381  rrxmval  23234  tdeglem4  23865  tayl0  24161  itgulm2  24208  pserulm  24221  efabl  24341  efsubm  24342  lmif  25722  islmib  25724  nbusgrf1o1  26316  cusgrfilem3  26409  vtxdgfval  26419  wlkiswwlks2  26829  wwlksnextbij  26865  clwlkclwwlklem1  26965  grpoinvfval  27504  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  aciunf1lem  29590  indv  30202  indval  30203  ofcfval  30288  ofcfval3  30292  omsval  30483  carsgclctunlem2  30509  pmeasadd  30515  sitgclg  30532  bnj1366  31026  ptpconn  31341  fwddifval  32394  tailfval  32492  curfv  33519  matunitlindflem1  33535  matunitlindflem2  33536  upixp  33654  pw2f1ocnv  37921  kelac1  37950  rfovd  38612  rfovfvd  38613  fsovrfovd  38620  fsovfvd  38621  dssmapfvd  38628  dssmapfv2d  38629  dssmapf1od  38632  fmulcl  40131  fmuldfeqlem1  40132  dvnmul  40476  dvnprodlem2  40480  stoweidlem31  40566  stoweidlem42  40577  stoweidlem48  40583  etransclem1  40770  etransclem4  40773  etransclem13  40782  etransclem17  40786  0ome  41064  hoicvr  41083  hsphoif  41111  hsphoival  41114  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  ovnhoilem2  41137  ovnlecvr2  41145  ovncvr2  41146  hoidifhspval2  41150  hspmbllem2  41162  sprbisymrel  42074  uspgrbisymrelALT  42088  funcrngcsetc  42323  funcringcsetc  42360  scmsuppss  42478  rmfsupp  42480  scmfsupp  42484  mptcfsupp  42486  lincresunit2  42592  offval0  42624
  Copyright terms: Public domain W3C validator