Theorem mptexg 7218

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 6583	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2733	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6237	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5322	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 689	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7216	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3947   ↦ cmpt 5230  dom cdm 5675  Fun wfun 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is referenced by:  mptex  7220  mptexd  7221  ovmpt3rab1  7659  offval  7674  abrexexgOLD  7943  xpexgALT  7963  offval3  7964  suppssov1  8178  suppssfv  8182  iunon  8334  onoviun  8338  mptelixpg  8925  cantnfp1lem1  9669  updjud  9925  coftr  10264  axcc3  10429  reps  14716  wrd2f1tovbij  14907  restval  17368  resf1st  17840  resf2nd  17841  funcres  17842  vrmdfval  18733  symgfixfolem1  19299  pmtrval  19312  pmtrrn  19318  pmtrfrn  19319  sylow1lem4  19462  sylow3lem2  19489  sylow3lem3  19490  uvcfval  21323  uvcval  21324  uvcff  21330  uvcresum  21332  psrass1lemOLD  21475  psrass1lem  21478  opsrval  21583  selvfval  21662  psropprmul  21742  mavmuldm  22034  mat2pmatfval  22207  cpm2mfval  22233  chpmatfval  22314  ntrfval  22510  clsfval  22511  neifval  22585  lpfval  22624  ptcnplem  23107  upxp  23109  fmfnfmlem3  23442  fmfnfmlem4  23443  ustuqtoplem  23726  ustuqtop0  23727  utopsnneiplem  23734  rrxmval  24904  tdeglem4OLD  25560  tayl0  25856  itgulm2  25903  efabl  26041  tgjustr  27705  lmif  28016  islmib  28018  nbusgrf1o1  28607  cusgrfilem3  28694  vtxdgfval  28704  wlkiswwlks2  29109  wwlksnextbij  29136  clwlkclwwlklem1  29232  grpoinvfval  29753  acunirnmpt  31862  acunirnmpt2  31863  acunirnmpt2f  31864  aciunf1lem  31865  fnpreimac  31874  mptiffisupp  31893  frlmdim  32641  indv  32948  indval  32949  ofcfval3  33038  omsval  33230  carsgclctunlem2  33256  pmeasadd  33262  sitgclg  33279  bnj1366  33778  ptpconn  34162  fwddifval  35072  tailfval  35195  curfv  36406  matunitlindflem1  36422  matunitlindflem2  36423  upixp  36535  pw2f1ocnv  41709  kelac1  41738  rfovd  42685  fsovrfovd  42693  dssmapfvd  42701  dssmapfv2d  42702  fmulcl  44232  fmuldfeqlem1  44233  dvnmul  44594  dvnprodlem2  44598  stoweidlem31  44682  stoweidlem42  44693  stoweidlem48  44699  etransclem1  44886  etransclem4  44889  etransclem13  44898  etransclem17  44902  0ome  45180  hoicvr  45199  hsphoif  45227  hsphoival  45230  hoidmvlelem2  45247  hoidmvlelem3  45248  ovnhoilem1  45252  ovnhoilem2  45253  ovnlecvr2  45261  ovncvr2  45262  hoidifhspval2  45266  hspmbllem2  45278  fundcmpsurinjALT  46015  sprbisymrel  46102  uspgrbisymrelALT  46468  funcrngcsetc  46798  funcringcsetc  46835  scmsuppss  46950  rmfsupp  46952  scmfsupp  46956  mptcfsupp  46958  lincresunit2  47061  itcoval0mpt  47254  eufsn  47410