Theorem mptexg 7250

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

Step	Hyp	Ref	Expression
1		funmpt 6598	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2763	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6255	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5285	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 703	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7248	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ↦ cmpt 5189  dom cdm 5655  Fun wfun 6552

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566

This theorem is used by:  mptex  7252  mptexd  7253  ovmpt3rab1  7703  offval  7726  xpexgALT  8017  offval3  8018  suppssov1  8242  suppssov2  8243  suppssfv  8247  iunon  8375  onoviun  8379  curfv  8920  mptelixpg  8991  cantnfp1lem1  9706  updjud  10042  coftr  10378  axcc3  10543  indv  12349  indval  12350  reps  14949  wrd2f1tovbij  15142  restval  17626  resf1st  18098  resf2nd  18099  funcres  18100  vrmdfval  19081  symgfixfolem1  19682  pmtrval  19695  pmtrrn  19701  pmtrfrn  19702  sylow1lem4  19845  sylow3lem2  19872  sylow3lem3  19873  funcrngcsetc  20922  funcringcsetc  20956  uvcfval  22120  uvcval  22121  uvcff  22127  uvcresum  22129  psrass1lem  22271  opsrval  22385  selvfval  22458  psropprmul  22585  mavmuldm  22895  matunitlindflem1  23024  matunitlindflem2  23025  mat2pmatfval  23071  cpm2mfval  23097  chpmatfval  23178  ntrfval  23372  clsfval  23373  neifval  23447  lpfval  23486  ptcnplem  23970  upxp  23972  fmfnfmlem3  24305  fmfnfmlem4  24306  ustuqtoplem  24588  ustuqtop0  24589  utopsnneiplem  24596  rrxmval  25756  tayl0  26719  itgulm2  26766  efabl  26908  tgjustr  28966  lmif  29320  islmib  29322  nbusgrf1o1  29981  cusgrfilem3  30068  vtxdgfval  30078  wlkiswwlks2  30494  wwlksnextbij  30521  clwlkclwwlklem1  30620  grpoinvfval  31154  acunirnmpt  33325  acunirnmpt2  33326  aciunf1lem  33328  fnpreimac  33336  mptiffisupp  33357  frlmdim  34313  ofcfval3  34804  omsval  34995  carsgclctunlem2  35021  pmeasadd  35027  sitgclg  35044  bnj1366  35529  fwddifval  37105  tailfval  37338  upixp  38855  pw2f1ocnv  44237  kelac1  44258  rfovd  45193  fsovrfovd  45201  dssmapfvd  45209  dssmapfv2d  45210  fmulcl  46798  fmuldfeqlem1  46799  dvnmul  47158  dvnprodlem2  47162  stoweidlem31  47246  stoweidlem42  47257  stoweidlem48  47263  etransclem1  47450  etransclem4  47453  etransclem13  47462  etransclem17  47466  0ome  47744  hsphoif  47791  hsphoival  47794  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoilem1  47816  ovnhoilem2  47817  ovnlecvr2  47825  ovncvr2  47826  hoidifhspval2  47830  hspmbllem2  47842  fundcmpsurinjALT  48699  sprbisymrel  48786  uspgrbisymrelALT  49458  scmsuppss  49688  rmfsupp  49690  scmfsupp  49692  mptcfsupp  49694  lincresunit2  49795  itcoval0mpt  49983  eufsn  50158