Theorem mptex 7229

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7227. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)

Hypothesis

Ref	Expression
mptex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
mptex	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem mptex

Step	Hyp	Ref	Expression
1		mptex.1	. 2 ⊢ 𝐴 ∈ V
2		mptexg 7227	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546

This theorem is used by:  mptrabex  7231  mptfvmpt  7234  eufnfv  7235  fvresex  7972  ofmres  7996  noinfep  9661  cantnffval  9664  cnfcomlem  9700  cnfcom3clem  9706  ssttrcl  9716  ttrcltr  9717  ttrclselem2  9727  fseqenlem1  10103  dfacacn  10220  dfac12lem1  10222  infmap2  10295  ackbij2lem2  10317  ackbij2lem3  10318  fin23lem32  10422  konigthlem  10653  wunex2  10823  wuncval2  10832  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  mptnn0fsupp  14140  ccatfn  14717  ccatfval  14718  swrdval  14791  swrd00  14792  swrd0  14808  revval  14909  repsundef  14922  climmpt  15738  climle  15807  iserabs  15982  isumshft  16008  divcnvshft  16024  supcvg  16025  trireciplem  16031  expcnv  16033  explecnv  16034  geolim  16039  geo2lim  16044  cvgrat  16052  mertenslem2  16054  eftlub  16277  rpnnen2lem1  16382  rpnnen2lem2  16383  1arithlem1  17101  1arith  17105  vdwapval  17151  vdwlem6  17164  vdwlem9  17167  restfn  17595  cidffn  17852  idfu2nd  18052  idfu1st  18054  idfucl  18056  fucco  18140  homafval  18204  prf1  18374  prf2fval  18375  prfcl  18377  prf1st  18378  prf2nd  18379  curf1fval  18398  curf11  18400  curf12  18401  curf1cl  18402  curf2  18403  curfcl  18406  hof2val  18430  yonedalem3a  18448  yonedalem4a  18449  yonedalem4b  18450  yonedalem4c  18451  yonedalem3  18454  yonedainv  18455  lubfval  18522  glbfval  18535  smndex1gbasOLD  19099  smndex1gidOLD  19101  smndex1igidOLD  19103  smndex1mnd  19109  smndex1id  19110  smndex1n0mnd  19111  smndex2dbas  19113  smndex2hbas  19115  cntzfval  19534  psgnfval  19714  sylow1lem2  19813  sylow2blem1  19834  sylow2blem2  19835  sylow3lem1  19841  sylow3lem6  19846  pj1fval  19908  vrgpfval  19980  rgspnval  20864  lspfval  21248  sraval  21450  irinitoringc  21785  zrhval2  21814  aspval  22180  psrmulfval  22251  psrass1  22271  mvrval  22289  mplmon  22344  mplcoe1  22346  evlslem2  22388  mpfrcl  22394  evlsval  22395  evlsvvvallem2  22401  evlsvvval  22402  evlsvar  22404  mpfind  22424  selvvvval  22451  mhpfval  22459  psdval  22480  psdmul  22487  coe1fval  22523  psropprmul  22555  coe1mul2  22588  ply1coe  22616  evls1fval  22637  evls1val  22638  evl1fval  22646  evl1val  22647  submafval  22894  mdetfval  22901  madufval  22952  minmar1fval  22961  pmatcollpw2lem  23095  pm2mpval  23113  1stcfb  23763  ptbasfi  23900  dfac14  23937  fmval  24262  fmf  24264  flffval  24308  fcfval  24352  cnextval  24380  met1stc  24840  pcoval  25332  iscmet3lem3  25611  rrxsca  25717  mbflimsup  25987  mbflim  25989  itg1climres  26035  mbfi1fseqlem2  26037  mbfi1fseqlem4  26039  mbfi1fseqlem6  26041  mbfi1flimlem  26043  mbfmullem2  26045  itg2monolem1  26071  itg2addlem  26079  itg2cnlem1  26082  cpnfval  26252  mdegfval  26380  elply  26513  plyeq0lem  26529  plypf1  26531  geolim3  26666  ulmuni  26719  ulmcau  26722  ulmdvlem1  26727  ulmdvlem3  26729  mbfulm  26733  itgulm  26735  pserval  26737  dvradcnv  26748  pserdvlem2  26755  abelthlem1  26758  abelthlem3  26760  abelthlem6  26763  logtayl  26988  leibpi  27270  dfef2  27298  emcllem4  27326  emcllem6  27328  emcllem7  27329  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamcvg2  27382  basellem6  27413  sqff1o  27509  dchrptlem2  27592  dchrptlem3  27593  2lgslem1  27721  dchrisumlem3  27818  padicfval  27943  padicabvf  27958  mirval  29127  ishpg  29237  lmif  29290  islmib  29292  axlowdim  29539  crctcshlem3  30408  nmoofval  31364  pjhfval  31998  pjmfn  32317  hosmval  32337  hommval  32338  hodmval  32339  hfsmval  32340  hfmmval  32341  eigvalfval  32499  brafval  32545  kbfval  32554  rnbra  32709  bra11  32710  fpwrelmap  33325  qusima  33959  nsgmgc  33963  nsgqusf1o  33967  idlsrgtset  34040  extvfval  34164  mplvrpmga  34177  esplyval  34194  locfinreflem  34472  rspectopn  34499  zarcmplem  34513  ordtconnlem1  34556  xrhval  34650  sigapildsys  34795  sxbrsigalem2  34918  eulerpart  35014  dstfrvclim1  35110  ballotlemfval  35122  ballotlemsval  35141  signstfv  35192  vtsval  35266  fineqvnttrclse  35792  cvmliftlem5  36054  mrsubffval  36272  mrsubfval  36273  msubffval  36288  msubfval  36289  msubrn  36294  msubco  36296  msubvrs  36325  circum  36439  divcnvlin  36498  climlec3  36499  faclimlem2  36509  faclim2  36513  knoppcnlem1  37359  knoppcnlem6  37364  knoppcnlem7  37365  cnndvlem2  37404  bj-endval  38236  ptrest  38537  poimirlem17  38555  poimirlem20  38558  voliunnfl  38582  volsupnfl  38583  upixp  38663  sdclem2  38676  fdc  38679  lmclim2  38692  geomcau  38693  rrncmslem  38766  pclfvalN  40946  polfvalN  40961  trlset  41218  tendopl  41833  docafvalN  42179  dibfval  42198  dibopelvalN  42200  dibopelval2  42202  dibelval3  42204  dibn0  42210  dib0  42221  diblsmopel  42228  dicn0  42249  dihopelvalcpre  42305  dihatlat  42391  dihpN  42393  dochfval  42407  lcfrlem9  42607  hvmapfval  42816  hvmapval  42817  hdmap1fval  42853  hlhilset  42991  sticksstones10  43205  sticksstones12a  43207  aks6d1c6isolem2  43225  evlselv  43617  prjcrvfval  43667  mzpincl  43744  dfac11  44063  dfac21  44067  hbtlem1  44124  hbtlem7  44126  fsovd  45007  mnringmulrcld  45225  dvgrat  45295  radcnvrat  45297  hashnzfzclim  45305  uzmptshftfval  45329  dvradcnv2  45330  binomcxplemrat  45333  binomcxplemcvg  45337  binomcxplemdvsum  45338  binomcxplemnotnn0  45339  addrval  45447  subrval  45448  mulvval  45449  fmuldfeqlem1  46593  fmuldfeq  46594  clim1fr1  46612  climexp  46616  climneg  46621  climdivf  46623  divcnvg  46638  expfac  46666  climresmpt  46668  climsubmpt  46669  limsupval4  46803  climliminflimsupd  46810  liminfreuzlem  46811  liminfltlem  46813  liminfpnfuz  46825  dvsinax  46922  dvcosax  46935  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem1  46955  dvnprodlem2  46956  dvnprodlem3  46957  stoweidlem59  47068  wallispilem5  47078  wallispi  47079  stirlinglem1  47083  stirlinglem8  47090  stirlinglem14  47096  stirlinglem15  47097  dirkerval  47100  fourierdlem71  47186  fourierdlem103  47218  fourierdlem104  47219  fourierdlem112  47227  etransclem48  47291  salgensscntex  47353  sge0tsms  47389  nnfoctbdjlem  47464  isomenndlem  47539  ovnval  47550  ovncvrrp  47573  ovnsubaddlem1  47579  hsphoif  47585  hsphoival  47588  ovnhoilem2  47611  hoidifhspval  47617  ovncvr2  47620  hspmbllem2  47636  vonioolem1  47689  smfpimcclem  47816  smflimsuplem1  47829  smflimsuplem4  47832  smflimsuplem7  47835  smfliminflem  47839  fsupdm  47851  smfsupdmmbllem  47853  finfdm  47855  smfinfdmmbllem  47857  cfsetsnfsetfo  48129  isuspgrim0  48991  cycldlenngric  49025  isgrtri  49040  1aryenef  49756  2aryenef  49767  itcovalpclem2  49782  itcovalt2lem2  49787  ackvalsuc1mpt  49789  ackval0  49791  cofidvala  50223  cofidval  50226  isnatd  50330  swapfelvv  50370  swapf2fvala  50371  swapf1vala  50373  swapf2fn  50375  swapf2vala  50377  tposcurf1  50406  prcofelvv  50487  reldmprcof1  50488  reldmprcof2  50489  prcof1  50495  prcof2a  50496  prcof2  50497  idfudiag1bas  50631  idfudiag1  50632  lmdfval  50756  cmdfval  50757  aacllem  50938  crosspval  50953  veronesevald  50970