MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fex2 Unicode version

Theorem fex2 5484
Description: A function with bounded domain and range is a set. This version of fex 5835 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
fex2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  e.  _V )

Proof of Theorem fex2
StepHypRef Expression
1 fssxp 5483 . . 3  |-  ( F : A --> B  ->  F  C_  ( A  X.  B ) )
213ad2ant1 976 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  C_  ( A  X.  B ) )
3 xpexg 4882 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
433adant1 973 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
5 ssexg 4241 . 2  |-  ( ( F  C_  ( A  X.  B )  /\  ( A  X.  B )  e. 
_V )  ->  F  e.  _V )
62, 4, 5syl2anc 642 1  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    e. wcel 1710   _Vcvv 2864    C_ wss 3228    X. cxp 4769   -->wf 5333
This theorem is referenced by:  elmapg  6873  f1oen2g  6966  f1dom2g  6967  dom3d  6991  domssex2  7109  domssex  7110  mapxpen  7115  oismo  7345  wdomima2g  7390  ixpiunwdom  7395  dfac8clem  7749  ac5num  7753  acni2  7763  acnlem  7765  dfac4  7839  dfac2a  7846  axdc2lem  8164  axdc4lem  8171  axcclem  8173  ac6num  8196  axdclem2  8237  addex  10444  mulex  10445  seqf1olem2  11178  seqf1o  11179  ccatfn  11523  limsuple  12048  limsuplt  12049  limsupbnd1  12052  caucvgrlem  12242  prdsval  13454  prdsplusg  13457  prdsmulr  13458  prdsvsca  13459  prdsds  13462  prdshom  13465  plusffval  14478  gsumval  14551  frmdplusg  14575  vrmdfval  14577  odinf  14975  efgtf  15130  gsumval3  15290  staffval  15711  scaffval  15744  cnfldcj  16489  cnfldds  16492  xrsadd  16497  xrsmul  16498  xrsds  16520  ipffval  16658  ocvfval  16672  cnpfval  17070  iscnp2  17075  txcn  17426  fmval  17740  fmf  17742  tsmsval  17915  tsmsadd  17931  blfval  18049  nmfval  18213  tngnm  18269  tngngp2  18270  tngngpd  18271  tngngp  18272  nmoffn  18322  nmofval  18325  ishtpy  18574  tchex  18753  adjeu  22583  ismeas  23819  isismty  25848  rrnval  25874  hasheqf1oi  27483
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-xp 4777  df-rel 4778  df-cnv 4779  df-dm 4781  df-rn 4782  df-fun 5339  df-fn 5340  df-f 5341
  Copyright terms: Public domain W3C validator