MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fexd Structured version   Visualization version   GIF version

Theorem fexd 7178
Description: If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
fexd.1 (𝜑𝐹:𝐴𝐵)
fexd.2 (𝜑𝐴𝐶)
Assertion
Ref Expression
fexd (𝜑𝐹 ∈ V)

Proof of Theorem fexd
StepHypRef Expression
1 fexd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 fexd.2 . 2 (𝜑𝐴𝐶)
3 fex 7177 . 2 ((𝐹:𝐴𝐵𝐴𝐶) → 𝐹 ∈ V)
41, 2, 3syl2anc 585 1 (𝜑𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3444  wf 6493
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 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385
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 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505
This theorem is referenced by:  fidmfisupp  9318  fdmfisuppfi  9319  fsuppco2  9344  fsuppcor  9345  ixpiunwdom  9531  cnfcom3clem  9646  fin23lem32  10285  hasheqf1od  14259  hashf1lem1  14359  hashf1lem1OLD  14360  fz1isolem  14366  ramval  16885  imasval  17398  imasle  17410  pwsco1mhm  18647  efgtf  19509  gsumval3a  19685  gsumval3lem1  19687  gsumval3lem2  19688  gsumval3  19689  gsumzres  19691  gsumzf1o  19694  gsumzaddlem  19703  gsumzadd  19704  gsumzmhm  19719  gsumzoppg  19726  gsumpt  19744  gsum2dlem2  19753  prdslmodd  20445  dsmmsubg  21165  dsmmlss  21166  islindf2  21236  f1lindf  21244  islindf4  21260  gsumply1subr  21621  txcn  22993  prdstps  22996  qtopval2  23063  fmval  23310  tsmsres  23511  tsmsadd  23514  jensen  26354  pwrssmgc  31909  gsumpart  31946  ply1degltdimlem  32374  ofcfval4  32761  omsfval  32951  omssubadd  32957  carsgval  32960  sseqval  33045  hgt750lemg  33324  filnetlem4  34899  bj-finsumval0  35802  isrngod  36403  isgrpda  36460  iscringd  36503  sticksstones8  40607  limsupre  43968  limsupval3  44019  limsuppnfdlem  44028  limsupvaluz  44035  limsuppnflem  44037  limsupre2lem  44051  climuzlem  44070  climisp  44073  climxrrelem  44076  climxrre  44077  liminfval5  44092  limsupgtlem  44104  liminfvalxr  44110  liminflelimsupuz  44112  liminfgelimsupuz  44115  liminflimsupclim  44134  liminflbuz2  44142  xlimclim2lem  44166  climxlim2  44173  fourierdlem71  44504  fourierdlem80  44513  sge0val  44693  sge0f1o  44709  isomennd  44858  nsssmfmbflem  45105  itcovalendof  46841
  Copyright terms: Public domain W3C validator