Theorem mptexg 7219

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

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

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 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539

This theorem is used by:  mptex  7221  mptexd  7222  ovmpt3rab1  7671  offval  7691  xpexgALT  7982  offval3  7983  suppssov1  8198  suppssov2  8199  suppssfv  8203  iunon  8331  onoviun  8335  curfv  8876  mptelixpg  8947  cantnfp1lem1  9663  updjud  9996  coftr  10332  axcc3  10497  indv  12303  indval  12304  reps  14901  wrd2f1tovbij  15093  restval  17577  resf1st  18049  resf2nd  18050  funcres  18051  vrmdfval  19032  symgfixfolem1  19632  pmtrval  19645  pmtrrn  19651  pmtrfrn  19652  sylow1lem4  19795  sylow3lem2  19822  sylow3lem3  19823  funcrngcsetc  20872  funcringcsetc  20906  uvcfval  22070  uvcval  22071  uvcff  22077  uvcresum  22079  psrass1lem  22221  opsrval  22335  selvfval  22408  psropprmul  22535  mavmuldm  22845  matunitlindflem1  22974  matunitlindflem2  22975  mat2pmatfval  23021  cpm2mfval  23047  chpmatfval  23128  ntrfval  23322  clsfval  23323  neifval  23397  lpfval  23436  ptcnplem  23920  upxp  23922  fmfnfmlem3  24255  fmfnfmlem4  24256  ustuqtoplem  24538  ustuqtop0  24539  utopsnneiplem  24546  rrxmval  25706  tayl0  26671  itgulm2  26718  efabl  26860  tgjustr  28918  lmif  29272  islmib  29274  nbusgrf1o1  29933  cusgrfilem3  30020  vtxdgfval  30030  wlkiswwlks2  30446  wwlksnextbij  30473  clwlkclwwlklem1  30572  grpoinvfval  31106  acunirnmpt  33235  acunirnmpt2  33236  acunirnmpt2f  33237  aciunf1lem  33238  fnpreimac  33246  mptiffisupp  33268  frlmdim  34225  ofcfval3  34716  omsval  34908  carsgclctunlem2  34934  pmeasadd  34940  sitgclg  34957  bnj1366  35442  ptpconn  35967  fwddifval  36897  tailfval  37130  upixp  38631  pw2f1ocnv  43997  kelac1  44023  rfovd  44960  fsovrfovd  44968  dssmapfvd  44976  dssmapfv2d  44977  fmulcl  46537  fmuldfeqlem1  46538  dvnmul  46897  dvnprodlem2  46901  stoweidlem31  46985  stoweidlem42  46996  stoweidlem48  47002  etransclem1  47189  etransclem4  47192  etransclem13  47201  etransclem17  47205  0ome  47483  hsphoif  47530  hsphoival  47533  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoilem1  47555  ovnhoilem2  47556  ovnlecvr2  47564  ovncvr2  47565  hoidifhspval2  47569  hspmbllem2  47581  fundcmpsurinjALT  48438  sprbisymrel  48525  uspgrbisymrelALT  49197  scmsuppss  49427  rmfsupp  49429  scmfsupp  49431  mptcfsupp  49433  lincresunit2  49534  itcoval0mpt  49722  eufsn  49896