Theorem mptexg 7224

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902   ↦ cmpt 5190  dom cdm 5659  Fun wfun 6531

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  mptex  7226  mptexd  7227  ovmpt3rab1  7676  offval  7691  xpexgALT  7982  offval3  7983  suppssov1  8199  suppssov2  8200  suppssfv  8204  iunon  8332  onoviun  8336  curfv  8875  mptelixpg  8946  cantnfp1lem1  9661  updjud  9943  coftr  10279  axcc3  10444  indv  12248  indval  12249  reps  14845  wrd2f1tovbij  15037  restval  17517  resf1st  17989  resf2nd  17990  funcres  17991  vrmdfval  18971  symgfixfolem1  19571  pmtrval  19584  pmtrrn  19590  pmtrfrn  19591  sylow1lem4  19734  sylow3lem2  19761  sylow3lem3  19762  funcrngcsetc  20808  funcringcsetc  20842  uvcfval  22003  uvcval  22004  uvcff  22010  uvcresum  22012  psrass1lem  22154  opsrval  22268  selvfval  22341  psropprmul  22468  mavmuldm  22778  matunitlindflem1  22907  matunitlindflem2  22908  mat2pmatfval  22954  cpm2mfval  22980  chpmatfval  23061  ntrfval  23255  clsfval  23256  neifval  23330  lpfval  23369  ptcnplem  23853  upxp  23855  fmfnfmlem3  24188  fmfnfmlem4  24189  ustuqtoplem  24471  ustuqtop0  24472  utopsnneiplem  24479  rrxmval  25639  tayl0  26605  itgulm2  26652  efabl  26795  tgjustr  28823  lmif  29177  islmib  29179  nbusgrf1o1  29838  cusgrfilem3  29925  vtxdgfval  29935  wlkiswwlks2  30351  wwlksnextbij  30378  clwlkclwwlklem1  30477  grpoinvfval  31011  acunirnmpt  33140  acunirnmpt2  33141  acunirnmpt2f  33142  aciunf1lem  33143  fnpreimac  33151  mptiffisupp  33173  frlmdim  34129  ofcfval3  34620  omsval  34812  carsgclctunlem2  34838  pmeasadd  34844  sitgclg  34861  bnj1366  35346  ptpconn  35820  fwddifval  36750  tailfval  36999  upixp  38487  pw2f1ocnv  43886  kelac1  43912  rfovd  44849  fsovrfovd  44857  dssmapfvd  44865  dssmapfv2d  44866  fmulcl  46419  fmuldfeqlem1  46420  dvnmul  46779  dvnprodlem2  46783  stoweidlem31  46867  stoweidlem42  46878  stoweidlem48  46884  etransclem1  47071  etransclem4  47074  etransclem13  47083  etransclem17  47087  0ome  47365  hsphoif  47412  hsphoival  47415  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoilem1  47437  ovnhoilem2  47438  ovnlecvr2  47446  ovncvr2  47447  hoidifhspval2  47451  hspmbllem2  47463  fundcmpsurinjALT  48320  sprbisymrel  48407  uspgrbisymrelALT  49079  scmsuppss  49309  rmfsupp  49311  scmfsupp  49313  mptcfsupp  49315  lincresunit2  49416  itcoval0mpt  49604  eufsn  49778