Theorem mptexg 7226

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458   ⊆ wss 3908   ↦ cmpt 5197  dom cdm 5666  Fun wfun 6537

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551

This theorem is used by:  mptex  7228  mptexd  7229  ovmpt3rab1  7681  offval  7696  xpexgALT  7987  offval3  7988  suppssov1  8202  suppssov2  8203  suppssfv  8207  iunon  8335  onoviun  8339  mptelixpg  8942  cantnfp1lem1  9657  updjud  9939  coftr  10275  axcc3  10440  indv  12238  indval  12239  reps  14833  wrd2f1tovbij  15023  restval  17504  resf1st  17976  resf2nd  17977  funcres  17978  vrmdfval  18946  symgfixfolem1  19539  pmtrval  19552  pmtrrn  19558  pmtrfrn  19559  sylow1lem4  19702  sylow3lem2  19729  sylow3lem3  19730  funcrngcsetc  20776  funcringcsetc  20810  uvcfval  21971  uvcval  21972  uvcff  21978  uvcresum  21980  psrass1lem  22120  opsrval  22234  selvfval  22307  psropprmul  22434  mavmuldm  22744  mat2pmatfval  22917  cpm2mfval  22943  chpmatfval  23024  ntrfval  23218  clsfval  23219  neifval  23293  lpfval  23332  ptcnplem  23815  upxp  23817  fmfnfmlem3  24150  fmfnfmlem4  24151  ustuqtoplem  24433  ustuqtop0  24434  utopsnneiplem  24441  rrxmval  25601  tayl0  26562  itgulm2  26609  efabl  26752  tgjustr  28780  lmif  29131  islmib  29133  nbusgrf1o1  29757  cusgrfilem3  29844  vtxdgfval  29854  wlkiswwlks2  30261  wwlksnextbij  30288  clwlkclwwlklem1  30387  grpoinvfval  30911  acunirnmpt  33041  acunirnmpt2  33042  acunirnmpt2f  33043  aciunf1lem  33044  fnpreimac  33052  mptiffisupp  33075  frlmdim  34032  ofcfval3  34523  omsval  34715  carsgclctunlem2  34741  pmeasadd  34747  sitgclg  34764  bnj1366  35249  ptpconn  35746  fwddifval  36675  tailfval  36924  curfv  38292  matunitlindflem1  38308  matunitlindflem2  38309  upixp  38421  pw2f1ocnv  43805  kelac1  43831  rfovd  44768  fsovrfovd  44776  dssmapfvd  44784  dssmapfv2d  44785  fmulcl  46338  fmuldfeqlem1  46339  dvnmul  46698  dvnprodlem2  46702  stoweidlem31  46786  stoweidlem42  46797  stoweidlem48  46803  etransclem1  46990  etransclem4  46993  etransclem13  47002  etransclem17  47006  0ome  47284  hsphoif  47331  hsphoival  47334  hoidmvlelem2  47351  hoidmvlelem3  47352  ovnhoilem1  47356  ovnhoilem2  47357  ovnlecvr2  47365  ovncvr2  47366  hoidifhspval2  47370  hspmbllem2  47382  fundcmpsurinjALT  48202  sprbisymrel  48289  uspgrbisymrelALT  48961  scmsuppss  49192  rmfsupp  49194  scmfsupp  49196  mptcfsupp  49198  lincresunit2  49299  itcoval0mpt  49487  eufsn  49661