Theorem mptex 7228

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   ↦ cmpt 5197

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551

This theorem is used by:  mptrabex  7230  mptfvmpt  7233  eufnfv  7234  fvresex  7966  ofmres  7990  noinfep  9639  cantnffval  9642  cnfcomlem  9678  cnfcom3clem  9684  ssttrcl  9694  ttrcltr  9695  ttrclselem2  9705  fseqenlem1  10027  dfacacn  10144  dfac12lem1  10146  infmap2  10219  ackbij2lem2  10241  ackbij2lem3  10242  fin23lem32  10346  konigthlem  10571  wunex2  10741  wuncval2  10750  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  mptnn0fsupp  14053  ccatfn  14629  ccatfval  14630  swrdval  14703  swrd00  14704  swrd0  14720  revval  14821  repsundef  14834  climmpt  15648  climle  15717  iserabs  15893  isumshft  15919  divcnvshft  15935  supcvg  15936  trireciplem  15942  expcnv  15944  explecnv  15945  geolim  15950  geo2lim  15955  cvgrat  15963  mertenslem2  15965  eftlub  16190  rpnnen2lem1  16295  rpnnen2lem2  16296  1arithlem1  17008  1arith  17012  vdwapval  17058  vdwlem6  17071  vdwlem9  17074  restfn  17502  cidffn  17759  idfu2nd  17959  idfu1st  17961  idfucl  17963  fucco  18047  homafval  18111  prf1  18281  prf2fval  18282  prfcl  18284  prf1st  18285  prf2nd  18286  curf1fval  18305  curf11  18307  curf12  18308  curf1cl  18309  curf2  18310  curfcl  18313  hof2val  18337  yonedalem3a  18355  yonedalem4a  18356  yonedalem4b  18357  yonedalem4c  18358  yonedalem3  18361  yonedainv  18362  lubfval  18429  glbfval  18442  smndex1gbasOLD  18993  smndex1gidOLD  18995  smndex1igidOLD  18997  smndex1mnd  19003  smndex1id  19004  smndex1n0mnd  19005  smndex2dbas  19007  smndex2hbas  19009  cntzfval  19421  psgnfval  19601  sylow1lem2  19700  sylow2blem1  19721  sylow2blem2  19722  sylow3lem1  19728  sylow3lem6  19733  pj1fval  19795  vrgpfval  19867  rgspnval  20748  lspfval  21131  sraval  21333  irinitoringc  21666  zrhval2  21695  aspval  22059  psrmulfval  22130  psrass1  22150  mvrval  22168  mplmon  22223  mplcoe1  22225  evlslem2  22267  mpfrcl  22273  evlsval  22274  evlsvvvallem2  22280  evlsvvval  22281  evlsvar  22283  mpfind  22303  selvvvval  22330  mhpfval  22338  psdval  22359  psdmul  22366  coe1fval  22402  psropprmul  22434  coe1mul2  22467  ply1coe  22495  evls1fval  22516  evls1val  22517  evl1fval  22525  evl1val  22526  submafval  22773  mdetfval  22780  madufval  22831  minmar1fval  22840  pmatcollpw2lem  22971  pm2mpval  22989  1stcfb  23639  ptbasfi  23775  dfac14  23812  fmval  24137  fmf  24139  flffval  24183  fcfval  24227  cnextval  24255  met1stc  24715  pcoval  25207  iscmet3lem3  25486  rrxsca  25592  mbflimsup  25862  mbflim  25864  itg1climres  25910  mbfi1fseqlem2  25912  mbfi1fseqlem4  25914  mbfi1fseqlem6  25916  mbfi1flimlem  25918  mbfmullem2  25920  itg2monolem1  25946  itg2addlem  25954  itg2cnlem1  25957  cpnfval  26128  mdegfval  26256  elply  26389  plyeq0lem  26404  plypf1  26406  geolim3  26539  ulmuni  26592  ulmcau  26595  ulmdvlem1  26600  ulmdvlem3  26602  mbfulm  26606  itgulm  26608  pserval  26610  dvradcnv  26621  pserdvlem2  26628  abelthlem1  26631  abelthlem3  26633  abelthlem6  26636  logtayl  26862  leibpi  27144  dfef2  27172  emcllem4  27200  emcllem6  27202  emcllem7  27203  lgamgulmlem5  27234  lgamgulmlem6  27235  lgamcvg2  27256  basellem6  27287  sqff1o  27383  dchrptlem2  27466  dchrptlem3  27467  2lgslem1  27595  dchrisumlem3  27692  padicfval  27817  padicabvf  27832  mirval  28969  ishpg  29078  lmif  29131  islmib  29133  axlowdim  29348  crctcshlem3  30205  nmoofval  31151  pjhfval  31785  pjmfn  32104  hosmval  32124  hommval  32125  hodmval  32126  hfsmval  32127  hfmmval  32128  eigvalfval  32286  brafval  32332  kbfval  32341  rnbra  32496  bra11  32497  fpwrelmap  33115  qusima  33748  nsgmgc  33752  nsgqusf1o  33756  idlsrgtset  33829  extvfval  33953  mplvrpmga  33966  esplyval  33983  locfinreflem  34261  rspectopn  34288  zarcmplem  34302  ordtconnlem1  34345  xrhval  34439  sigapildsys  34584  sxbrsigalem2  34708  eulerpart  34804  dstfrvclim1  34900  ballotlemfval  34912  ballotlemsval  34931  signstfv  34982  vtsval  35056  fineqvnttrclse  35561  cvmliftlem5  35802  mrsubffval  36020  mrsubfval  36021  msubffval  36036  msubfval  36037  msubrn  36042  msubco  36044  msubvrs  36073  circum  36187  divcnvlin  36246  climlec3  36247  faclimlem2  36257  faclim2  36261  knoppcnlem1  37123  knoppcnlem6  37128  knoppcnlem7  37129  cnndvlem2  37168  bj-endval  38000  ptrest  38311  poimirlem17  38329  poimirlem20  38332  voliunnfl  38356  volsupnfl  38357  upixp  38421  sdclem2  38434  fdc  38437  lmclim2  38450  geomcau  38451  rrncmslem  38524  pclfvalN  40704  polfvalN  40719  trlset  40976  tendopl  41591  docafvalN  41937  dibfval  41956  dibopelvalN  41958  dibopelval2  41960  dibelval3  41962  dibn0  41968  dib0  41979  diblsmopel  41986  dicn0  42007  dihopelvalcpre  42063  dihatlat  42149  dihpN  42151  dochfval  42165  lcfrlem9  42365  hvmapfval  42574  hvmapval  42575  hdmap1fval  42611  hlhilset  42749  sticksstones10  42963  sticksstones12a  42965  aks6d1c6isolem2  42983  evlselv  43362  prjcrvfval  43404  mzpincl  43506  dfac11  43830  dfac21  43834  hbtlem1  43891  hbtlem7  43893  fsovd  44775  mnringmulrcld  44993  dvgrat  45063  radcnvrat  45065  hashnzfzclim  45073  uzmptshftfval  45097  dvradcnv2  45098  binomcxplemrat  45101  binomcxplemcvg  45105  binomcxplemdvsum  45106  binomcxplemnotnn0  45107  addrval  45215  subrval  45216  mulvval  45217  fmuldfeqlem1  46339  fmuldfeq  46340  clim1fr1  46358  climexp  46362  climneg  46367  climdivf  46369  divcnvg  46384  expfac  46412  climresmpt  46414  climsubmpt  46415  limsupval4  46549  climliminflimsupd  46556  liminfreuzlem  46557  liminfltlem  46559  liminfpnfuz  46571  dvsinax  46668  dvcosax  46681  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  stoweidlem59  46814  wallispilem5  46824  wallispi  46825  stirlinglem1  46829  stirlinglem8  46836  stirlinglem14  46842  stirlinglem15  46843  dirkerval  46846  fourierdlem71  46932  fourierdlem103  46964  fourierdlem104  46965  fourierdlem112  46973  etransclem48  47037  salgensscntex  47099  sge0tsms  47135  nnfoctbdjlem  47210  isomenndlem  47285  ovnval  47296  ovncvrrp  47319  ovnsubaddlem1  47325  hsphoif  47331  hsphoival  47334  ovnhoilem2  47357  hoidifhspval  47363  ovncvr2  47366  hspmbllem2  47382  vonioolem1  47435  smfpimcclem  47562  smflimsuplem1  47575  smflimsuplem4  47578  smflimsuplem7  47581  smfliminflem  47585  fsupdm  47597  smfsupdmmbllem  47599  finfdm  47601  smfinfdmmbllem  47603  cfsetsnfsetfo  47838  isuspgrim0  48700  cycldlenngric  48734  isgrtri  48749  1aryenef  49466  2aryenef  49477  itcovalpclem2  49492  itcovalt2lem2  49497  ackvalsuc1mpt  49499  ackval0  49501  cofidvala  49935  cofidval  49938  isnatd  50042  swapfelvv  50082  swapf2fvala  50083  swapf1vala  50085  swapf2fn  50087  swapf2vala  50089  tposcurf1  50118  prcofelvv  50199  reldmprcof1  50200  reldmprcof2  50201  prcof1  50207  prcof2a  50208  prcof2  50209  idfudiag1bas  50343  idfudiag1  50344  lmdfval  50468  cmdfval  50469  aacllem  50662  crosspval  50677