Theorem mptexg 7223

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949   ↦ cmpt 5232  dom cdm 5677  Fun wfun 6538

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 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428

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 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552

This theorem is referenced by:  mptex  7225  mptexd  7226  ovmpt3rab1  7664  offval  7679  abrexexgOLD  7948  xpexgALT  7968  offval3  7969  suppssov1  8183  suppssfv  8187  iunon  8339  onoviun  8343  mptelixpg  8929  cantnfp1lem1  9673  updjud  9929  coftr  10268  axcc3  10433  reps  14720  wrd2f1tovbij  14911  restval  17372  resf1st  17844  resf2nd  17845  funcres  17846  vrmdfval  18737  symgfixfolem1  19306  pmtrval  19319  pmtrrn  19325  pmtrfrn  19326  sylow1lem4  19469  sylow3lem2  19496  sylow3lem3  19497  uvcfval  21339  uvcval  21340  uvcff  21346  uvcresum  21348  psrass1lemOLD  21493  psrass1lem  21496  opsrval  21601  selvfval  21680  psropprmul  21760  mavmuldm  22052  mat2pmatfval  22225  cpm2mfval  22251  chpmatfval  22332  ntrfval  22528  clsfval  22529  neifval  22603  lpfval  22642  ptcnplem  23125  upxp  23127  fmfnfmlem3  23460  fmfnfmlem4  23461  ustuqtoplem  23744  ustuqtop0  23745  utopsnneiplem  23752  rrxmval  24922  tdeglem4OLD  25578  tayl0  25874  itgulm2  25921  efabl  26059  tgjustr  27756  lmif  28067  islmib  28069  nbusgrf1o1  28658  cusgrfilem3  28745  vtxdgfval  28755  wlkiswwlks2  29160  wwlksnextbij  29187  clwlkclwwlklem1  29283  grpoinvfval  29806  acunirnmpt  31915  acunirnmpt2  31916  acunirnmpt2f  31917  aciunf1lem  31918  fnpreimac  31927  mptiffisupp  31946  frlmdim  32727  indv  33041  indval  33042  ofcfval3  33131  omsval  33323  carsgclctunlem2  33349  pmeasadd  33355  sitgclg  33372  bnj1366  33871  ptpconn  34255  fwddifval  35165  tailfval  35305  curfv  36516  matunitlindflem1  36532  matunitlindflem2  36533  upixp  36645  pw2f1ocnv  41824  kelac1  41853  rfovd  42800  fsovrfovd  42808  dssmapfvd  42816  dssmapfv2d  42817  fmulcl  44345  fmuldfeqlem1  44346  dvnmul  44707  dvnprodlem2  44711  stoweidlem31  44795  stoweidlem42  44806  stoweidlem48  44812  etransclem1  44999  etransclem4  45002  etransclem13  45011  etransclem17  45015  0ome  45293  hoicvr  45312  hsphoif  45340  hsphoival  45343  hoidmvlelem2  45360  hoidmvlelem3  45361  ovnhoilem1  45365  ovnhoilem2  45366  ovnlecvr2  45374  ovncvr2  45375  hoidifhspval2  45379  hspmbllem2  45391  fundcmpsurinjALT  46128  sprbisymrel  46215  uspgrbisymrelALT  46581  funcrngcsetc  46944  funcringcsetc  46981  scmsuppss  47096  rmfsupp  47098  scmfsupp  47102  mptcfsupp  47104  lincresunit2  47207  itcoval0mpt  47400  eufsn  47556