Theorem mptex 7223

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7221. (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 7221	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  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 referenced by:  mptrabex  7225  mptfvmpt  7228  eufnfv  7229  fvresex  7958  ofmres  7982  noinfep  9630  cantnffval  9633  cnfcomlem  9669  cnfcom3clem  9675  ssttrcl  9685  ttrcltr  9686  ttrclselem2  9696  fseqenlem1  10009  dfacacn  10126  dfac12lem1  10128  infmap2  10201  ackbij2lem2  10223  ackbij2lem3  10224  fin23lem32  10329  konigthlem  10554  wunex2  10724  wuncval2  10733  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  mptnn0fsupp  14035  ccatfn  14611  ccatfval  14612  swrdval  14683  swrd00  14684  swrd0  14698  revval  14799  repsundef  14810  climmpt  15624  climle  15693  iserabs  15869  isumshft  15895  divcnvshft  15911  supcvg  15912  trireciplem  15918  expcnv  15920  explecnv  15921  geolim  15926  geo2lim  15931  cvgrat  15939  mertenslem2  15941  eftlub  16166  rpnnen2lem1  16271  rpnnen2lem2  16272  1arithlem1  16984  1arith  16988  vdwapval  17034  vdwlem6  17047  vdwlem9  17050  restfn  17478  cidffn  17735  idfu2nd  17935  idfu1st  17937  idfucl  17939  fucco  18023  homafval  18087  prf1  18257  prf2fval  18258  prfcl  18260  prf1st  18261  prf2nd  18262  curf1fval  18281  curf11  18283  curf12  18284  curf1cl  18285  curf2  18286  curfcl  18289  hof2val  18313  yonedalem3a  18331  yonedalem4a  18332  yonedalem4b  18333  yonedalem4c  18334  yonedalem3  18337  yonedainv  18338  lubfval  18405  glbfval  18418  smndex1gbasOLD  18963  smndex1gidOLD  18965  smndex1igidOLD  18967  smndex1mnd  18973  smndex1id  18974  smndex1n0mnd  18975  smndex2dbas  18977  smndex2hbas  18979  cntzfval  19391  psgnfval  19571  sylow1lem2  19670  sylow2blem1  19691  sylow2blem2  19692  sylow3lem1  19698  sylow3lem6  19703  pj1fval  19765  vrgpfval  19837  rgspnval  20698  lspfval  21075  sraval  21277  irinitoringc  21610  zrhval2  21639  aspval  22003  psrmulfval  22074  psrass1  22094  mvrval  22112  mplmon  22167  mplcoe1  22169  evlslem2  22211  mpfrcl  22217  evlsval  22218  evlsvvvallem2  22224  evlsvvval  22225  evlsvar  22227  mpfind  22247  selvvvval  22274  mhpfval  22282  psdval  22303  psdmul  22310  coe1fval  22346  psropprmul  22378  coe1mul2  22411  ply1coe  22439  evls1fval  22460  evls1val  22461  evl1fval  22469  evl1val  22470  submafval  22717  mdetfval  22724  madufval  22775  minmar1fval  22784  pmatcollpw2lem  22915  pm2mpval  22933  1stcfb  23583  ptbasfi  23719  dfac14  23756  fmval  24081  fmf  24083  flffval  24127  fcfval  24171  cnextval  24199  met1stc  24659  pcoval  25151  iscmet3lem3  25430  rrxsca  25536  mbflimsup  25806  mbflim  25808  itg1climres  25854  mbfi1fseqlem2  25856  mbfi1fseqlem4  25858  mbfi1fseqlem6  25860  mbfi1flimlem  25862  mbfmullem2  25864  itg2monolem1  25890  itg2addlem  25898  itg2cnlem1  25901  cpnfval  26072  mdegfval  26200  elply  26333  plyeq0lem  26348  plypf1  26350  geolim3  26481  ulmuni  26533  ulmcau  26536  ulmdvlem1  26541  ulmdvlem3  26543  mbfulm  26547  itgulm  26549  pserval  26551  dvradcnv  26562  pserdvlem2  26569  abelthlem1  26572  abelthlem3  26574  abelthlem6  26577  logtayl  26803  leibpi  27085  dfef2  27113  emcllem4  27141  emcllem6  27143  emcllem7  27144  lgamgulmlem5  27175  lgamgulmlem6  27176  lgamcvg2  27197  basellem6  27228  sqff1o  27324  dchrptlem2  27407  dchrptlem3  27408  2lgslem1  27536  dchrisumlem3  27633  padicfval  27758  padicabvf  27773  mirval  28910  ishpg  29019  lmif  29072  islmib  29074  axlowdim  29289  crctcshlem3  30146  nmoofval  31092  pjhfval  31726  pjmfn  32045  hosmval  32065  hommval  32066  hodmval  32067  hfsmval  32068  hfmmval  32069  eigvalfval  32227  brafval  32273  kbfval  32282  rnbra  32437  bra11  32438  fpwrelmap  33056  qusima  33695  nsgmgc  33699  nsgqusf1o  33703  idlsrgtset  33776  extvfval  33900  mplvrpmga  33913  esplyval  33930  locfinreflem  34208  rspectopn  34235  zarcmplem  34249  ordtconnlem1  34292  xrhval  34386  sigapildsys  34530  sxbrsigalem2  34654  eulerpart  34750  dstfrvclim1  34846  ballotlemfval  34858  ballotlemsval  34877  signstfv  34928  vtsval  35002  fineqvnttrclse  35515  cvmliftlem5  35759  mrsubffval  35977  mrsubfval  35978  msubffval  35993  msubfval  35994  msubrn  35999  msubco  36001  msubvrs  36030  circum  36144  divcnvlin  36203  climlec3  36204  faclimlem2  36214  faclim2  36218  knoppcnlem1  37060  knoppcnlem6  37065  knoppcnlem7  37066  cnndvlem2  37105  bj-endval  37937  ptrest  38248  poimirlem17  38266  poimirlem20  38269  voliunnfl  38293  volsupnfl  38294  upixp  38358  sdclem2  38371  fdc  38374  lmclim2  38387  geomcau  38388  rrncmslem  38461  pclfvalN  40641  polfvalN  40656  trlset  40913  tendopl  41528  docafvalN  41874  dibfval  41893  dibopelvalN  41895  dibopelval2  41897  dibelval3  41899  dibn0  41905  dib0  41916  diblsmopel  41923  dicn0  41944  dihopelvalcpre  42000  dihatlat  42086  dihpN  42088  dochfval  42102  lcfrlem9  42302  hvmapfval  42511  hvmapval  42512  hdmap1fval  42548  hlhilset  42686  sticksstones10  42900  sticksstones12a  42902  aks6d1c6isolem2  42920  evlselv  43301  prjcrvfval  43343  mzpincl  43445  dfac11  43769  dfac21  43773  hbtlem1  43830  hbtlem7  43832  fsovd  44714  mnringmulrcld  44932  dvgrat  45002  radcnvrat  45004  hashnzfzclim  45012  uzmptshftfval  45036  dvradcnv2  45037  binomcxplemrat  45040  binomcxplemcvg  45044  binomcxplemdvsum  45045  binomcxplemnotnn0  45046  addrval  45154  subrval  45155  mulvval  45156  fmuldfeqlem1  46278  fmuldfeq  46279  clim1fr1  46297  climexp  46301  climneg  46306  climdivf  46308  divcnvg  46323  expfac  46351  climresmpt  46353  climsubmpt  46354  limsupval4  46488  climliminflimsupd  46495  liminfreuzlem  46496  liminfltlem  46498  liminfpnfuz  46510  dvsinax  46607  dvcosax  46620  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvnprodlem1  46640  dvnprodlem2  46641  dvnprodlem3  46642  stoweidlem59  46753  wallispilem5  46763  wallispi  46764  stirlinglem1  46768  stirlinglem8  46775  stirlinglem14  46781  stirlinglem15  46782  dirkerval  46785  fourierdlem71  46871  fourierdlem103  46903  fourierdlem104  46904  fourierdlem112  46912  etransclem48  46976  salgensscntex  47038  sge0tsms  47074  nnfoctbdjlem  47149  isomenndlem  47224  ovnval  47235  ovncvrrp  47258  ovnsubaddlem1  47264  hsphoif  47270  hsphoival  47273  ovnhoilem2  47296  hoidifhspval  47302  ovncvr2  47305  hspmbllem2  47321  vonioolem1  47374  smfpimcclem  47501  smflimsuplem1  47514  smflimsuplem4  47517  smflimsuplem7  47520  smfliminflem  47524  fsupdm  47536  smfsupdmmbllem  47538  finfdm  47540  smfinfdmmbllem  47542  cfsetsnfsetfo  47774  isuspgrim0  48636  cycldlenngric  48670  isgrtri  48685  1aryenef  49402  2aryenef  49413  itcovalpclem2  49428  itcovalt2lem2  49433  ackvalsuc1mpt  49435  ackval0  49437  cofidvala  49871  cofidval  49874  isnatd  49978  swapfelvv  50018  swapf2fvala  50019  swapf1vala  50021  swapf2fn  50023  swapf2vala  50025  tposcurf1  50054  prcofelvv  50135  reldmprcof1  50136  reldmprcof2  50137  prcof1  50143  prcof2a  50144  prcof2  50145  idfudiag1bas  50279  idfudiag1  50280  lmdfval  50404  cmdfval  50405  aacllem  50578