Theorem mptexg 7220

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 6571	. 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)
2		eqid 2760	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 6237	. . 3 ⊢ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴
4		ssexg 5284	. . 3 ⊢ ((dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
5	3, 4	mpan 703	. 2 ⊢ (𝐴 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
6		funex 7218	. 2 ⊢ ((Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899   ↦ cmpt 5186  dom cdm 5655  Fun wfun 6527

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  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 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541

This theorem is used by:  mptex  7222  mptexd  7223  ovmpt3rab1  7672  offval  7687  xpexgALT  7978  offval3  7979  suppssov1  8195  suppssov2  8196  suppssfv  8200  iunon  8328  onoviun  8332  curfv  8871  mptelixpg  8942  cantnfp1lem1  9657  updjud  9939  coftr  10275  axcc3  10440  indv  12244  indval  12245  reps  14841  wrd2f1tovbij  15033  restval  17511  resf1st  17983  resf2nd  17984  funcres  17985  vrmdfval  18965  symgfixfolem1  19565  pmtrval  19578  pmtrrn  19584  pmtrfrn  19585  sylow1lem4  19728  sylow3lem2  19755  sylow3lem3  19756  funcrngcsetc  20802  funcringcsetc  20836  uvcfval  21997  uvcval  21998  uvcff  22004  uvcresum  22006  psrass1lem  22148  opsrval  22262  selvfval  22335  psropprmul  22462  mavmuldm  22772  matunitlindflem1  22901  matunitlindflem2  22902  mat2pmatfval  22948  cpm2mfval  22974  chpmatfval  23055  ntrfval  23249  clsfval  23250  neifval  23324  lpfval  23363  ptcnplem  23847  upxp  23849  fmfnfmlem3  24182  fmfnfmlem4  24183  ustuqtoplem  24465  ustuqtop0  24466  utopsnneiplem  24473  rrxmval  25633  tayl0  26598  itgulm2  26645  efabl  26787  tgjustr  28815  lmif  29169  islmib  29171  nbusgrf1o1  29830  cusgrfilem3  29917  vtxdgfval  29927  wlkiswwlks2  30343  wwlksnextbij  30370  clwlkclwwlklem1  30469  grpoinvfval  31003  acunirnmpt  33132  acunirnmpt2  33133  acunirnmpt2f  33134  aciunf1lem  33135  fnpreimac  33143  mptiffisupp  33165  frlmdim  34121  ofcfval3  34612  omsval  34804  carsgclctunlem2  34830  pmeasadd  34836  sitgclg  34853  bnj1366  35338  ptpconn  35812  fwddifval  36742  tailfval  36991  upixp  38479  pw2f1ocnv  43878  kelac1  43904  rfovd  44841  fsovrfovd  44849  dssmapfvd  44857  dssmapfv2d  44858  fmulcl  46411  fmuldfeqlem1  46412  dvnmul  46771  dvnprodlem2  46775  stoweidlem31  46859  stoweidlem42  46870  stoweidlem48  46876  etransclem1  47063  etransclem4  47066  etransclem13  47075  etransclem17  47079  0ome  47357  hsphoif  47404  hsphoival  47407  hoidmvlelem2  47424  hoidmvlelem3  47425  ovnhoilem1  47429  ovnhoilem2  47430  ovnlecvr2  47438  ovncvr2  47439  hoidifhspval2  47443  hspmbllem2  47455  fundcmpsurinjALT  48312  sprbisymrel  48399  uspgrbisymrelALT  49071  scmsuppss  49301  rmfsupp  49303  scmfsupp  49305  mptcfsupp  49307  lincresunit2  49408  itcoval0mpt  49596  eufsn  49770