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 2144  Vcvv 3450   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  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  9664  cantnffval  9667  cnfcomlem  9703  cnfcom3clem  9709  ssttrcl  9719  ttrcltr  9720  ttrclselem2  9730  fseqenlem1  10106  dfacacn  10223  dfac12lem1  10225  infmap2  10298  ackbij2lem2  10320  ackbij2lem3  10321  fin23lem32  10425  konigthlem  10656  wunex2  10826  wuncval2  10835  rpnnen1lem1  13109  rpnnen1lem3  13110  rpnnen1lem5  13112  mptnn0fsupp  14143  ccatfn  14720  ccatfval  14721  swrdval  14795  swrd00  14796  swrd0  14812  revval  14913  repsundef  14926  climmpt  15743  climle  15812  iserabs  15987  isumshft  16013  divcnvshft  16029  supcvg  16030  trireciplem  16036  expcnv  16038  explecnv  16039  geolim  16044  geo2lim  16049  cvgrat  16057  mertenslem2  16059  eftlub  16282  rpnnen2lem1  16387  rpnnen2lem2  16388  1arithlem1  17106  1arith  17110  vdwapval  17156  vdwlem6  17169  vdwlem9  17172  restfn  17600  cidffn  17857  idfu2nd  18057  idfu1st  18059  idfucl  18061  fucco  18145  homafval  18209  prf1  18379  prf2fval  18380  prfcl  18382  prf1st  18383  prf2nd  18384  curf1fval  18403  curf11  18405  curf12  18406  curf1cl  18407  curf2  18408  curfcl  18411  hof2val  18435  yonedalem3a  18453  yonedalem4a  18454  yonedalem4b  18455  yonedalem4c  18456  yonedalem3  18459  yonedainv  18460  lubfval  18527  glbfval  18540  smndex1gbasOLD  19104  smndex1gidOLD  19106  smndex1igidOLD  19108  smndex1mnd  19114  smndex1id  19115  smndex1n0mnd  19116  smndex2dbas  19118  smndex2hbas  19120  cntzfval  19539  psgnfval  19719  sylow1lem2  19818  sylow2blem1  19839  sylow2blem2  19840  sylow3lem1  19846  sylow3lem6  19851  pj1fval  19913  vrgpfval  19985  rgspnval  20869  lspfval  21253  sraval  21455  irinitoringc  21790  zrhval2  21819  aspval  22185  psrmulfval  22256  psrass1  22276  mvrval  22294  mplmon  22349  mplcoe1  22351  evlslem2  22393  mpfrcl  22399  evlsval  22400  evlsvvvallem2  22406  evlsvvval  22407  evlsvar  22409  mpfind  22429  selvvvval  22456  mhpfval  22464  psdval  22485  psdmul  22492  coe1fval  22528  psropprmul  22560  coe1mul2  22593  ply1coe  22621  evls1fval  22642  evls1val  22643  evl1fval  22651  evl1val  22652  submafval  22899  mdetfval  22906  madufval  22957  minmar1fval  22966  pmatcollpw2lem  23100  pm2mpval  23118  1stcfb  23768  ptbasfi  23905  dfac14  23942  fmval  24267  fmf  24269  flffval  24313  fcfval  24357  cnextval  24385  met1stc  24845  pcoval  25337  iscmet3lem3  25616  rrxsca  25722  mbflimsup  25992  mbflim  25994  itg1climres  26040  mbfi1fseqlem2  26042  mbfi1fseqlem4  26044  mbfi1fseqlem6  26046  mbfi1flimlem  26048  mbfmullem2  26050  itg2monolem1  26076  itg2addlem  26084  itg2cnlem1  26087  cpnfval  26257  mdegfval  26385  elply  26518  plyeq0lem  26534  plypf1  26536  geolim3  26671  ulmuni  26724  ulmcau  26727  ulmdvlem1  26732  ulmdvlem3  26734  mbfulm  26738  itgulm  26740  pserval  26742  dvradcnv  26753  pserdvlem2  26760  abelthlem1  26763  abelthlem3  26765  abelthlem6  26768  logtayl  26993  leibpi  27275  dfef2  27303  emcllem4  27331  emcllem6  27333  emcllem7  27334  lgamgulmlem5  27365  lgamgulmlem6  27366  lgamcvg2  27387  basellem6  27418  sqff1o  27514  dchrptlem2  27597  dchrptlem3  27598  2lgslem1  27726  dchrisumlem3  27823  padicfval  27948  padicabvf  27963  mirval  29132  ishpg  29242  lmif  29295  islmib  29297  axlowdim  29544  crctcshlem3  30413  nmoofval  31369  pjhfval  32003  pjmfn  32322  hosmval  32342  hommval  32343  hodmval  32344  hfsmval  32345  hfmmval  32346  eigvalfval  32504  brafval  32550  kbfval  32559  rnbra  32714  bra11  32715  fpwrelmap  33371  qusima  34005  nsgmgc  34009  nsgqusf1o  34013  idlsrgtset  34086  extvfval  34210  mplvrpmga  34223  esplyval  34240  locfinreflem  34518  rspectopn  34545  zarcmplem  34559  ordtconnlem1  34602  xrhval  34696  sigapildsys  34841  sxbrsigalem2  34964  eulerpart  35060  dstfrvclim1  35156  ballotlemfval  35168  ballotlemsval  35187  signstfv  35238  vtsval  35312  fineqvnttrclse  35848  cvmliftlem5  36140  mrsubffval  36358  mrsubfval  36359  msubffval  36374  msubfval  36375  msubrn  36380  msubco  36382  msubvrs  36411  circum  36525  mirimanoffr  36546  divcnvlin  36590  climlec3  36591  faclimlem2  36601  faclim2  36605  knoppcnlem1  37451  knoppcnlem6  37456  knoppcnlem7  37457  cnndvlem2  37496  bj-endval  38329  ptrest  38630  poimirlem17  38648  poimirlem20  38651  voliunnfl  38675  volsupnfl  38676  upixp  38756  sdclem2  38769  fdc  38772  lmclim2  38785  geomcau  38786  rrncmslem  38859  pclfvalN  41039  polfvalN  41054  trlset  41311  tendopl  41926  docafvalN  42272  dibfval  42291  dibopelvalN  42293  dibopelval2  42295  dibelval3  42297  dibn0  42303  dib0  42314  diblsmopel  42321  dicn0  42342  dihopelvalcpre  42398  dihatlat  42484  dihpN  42486  dochfval  42500  lcfrlem9  42700  hvmapfval  42909  hvmapval  42910  hdmap1fval  42946  hlhilset  43084  sticksstones10  43298  sticksstones12a  43300  aks6d1c6isolem2  43318  evlselv  43710  prjcrvfval  43760  mzpincl  43838  dfac11  44157  dfac21  44161  hbtlem1  44218  hbtlem7  44220  fsovd  45101  mnringmulrcld  45319  dvgrat  45389  radcnvrat  45391  hashnzfzclim  45399  uzmptshftfval  45423  dvradcnv2  45424  binomcxplemrat  45427  binomcxplemcvg  45431  binomcxplemdvsum  45432  binomcxplemnotnn0  45433  addrval  45541  subrval  45542  mulvval  45543  fmuldfeqlem1  46687  fmuldfeq  46688  clim1fr1  46706  climexp  46710  climneg  46715  climdivf  46717  divcnvg  46732  expfac  46760  climresmpt  46762  climsubmpt  46763  limsupval4  46897  climliminflimsupd  46904  liminfreuzlem  46905  liminfltlem  46907  liminfpnfuz  46919  dvsinax  47016  dvcosax  47029  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvnprodlem1  47049  dvnprodlem2  47050  dvnprodlem3  47051  stoweidlem59  47162  wallispilem5  47172  wallispi  47173  stirlinglem1  47177  stirlinglem8  47184  stirlinglem14  47190  stirlinglem15  47191  dirkerval  47194  fourierdlem71  47280  fourierdlem103  47312  fourierdlem104  47313  fourierdlem112  47321  etransclem48  47385  salgensscntex  47447  sge0tsms  47483  nnfoctbdjlem  47558  isomenndlem  47633  ovnval  47644  ovncvrrp  47667  ovnsubaddlem1  47673  hsphoif  47679  hsphoival  47682  ovnhoilem2  47705  hoidifhspval  47711  ovncvr2  47714  hspmbllem2  47730  vonioolem1  47783  smfpimcclem  47910  smflimsuplem1  47923  smflimsuplem4  47926  smflimsuplem7  47929  smfliminflem  47933  fsupdm  47945  smfsupdmmbllem  47947  finfdm  47949  smfinfdmmbllem  47951  cfsetsnfsetfo  48223  isuspgrim0  49085  cycldlenngric  49119  isgrtri  49134  1aryenef  49850  2aryenef  49861  itcovalpclem2  49876  itcovalt2lem2  49881  ackvalsuc1mpt  49883  ackval0  49885  fnmpompt  50074  ovmpomptd  50075  cofidvala  50325  cofidval  50328  isnatd  50432  swapfelvv  50478  swapf2fvala  50479  swapf1vala  50481  swapf2fn  50483  swapf2vala  50485  tposcurf1  50514  postcof1st  50591  postcof2nd  50592  postcof2  50593  prcofelvv  50608  reldmprcof1  50609  reldmprcof2  50610  prcof1  50616  prcof2a  50617  prcof2  50618  idfudiag1bas  50752  idfudiag1  50753  fuconuniqlem  50874  fuconuniqvalslem  50876  lmdfval  50925  cmdfval  50926  aacllem  51107  crosspval  51122  veronesevald  51139