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

Theorem fex2 5401
Description: A function with bounded domain and range is a set. This version of fex 5749 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 5400 . . 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 4800 . . 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 4160 . 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 1684   _Vcvv 2788    C_ wss 3152    X. cxp 4687   -->wf 5251
This theorem is referenced by:  elmapg  6785  f1oen2g  6878  f1dom2g  6879  dom3d  6903  domssex2  7021  domssex  7022  mapxpen  7027  oismo  7255  wdomima2g  7300  ixpiunwdom  7305  dfac8clem  7659  ac5num  7663  acni2  7673  acnlem  7675  dfac4  7749  dfac2a  7756  axdc2lem  8074  axdc4lem  8081  axcclem  8083  ac6num  8106  axdclem2  8147  addex  10352  mulex  10353  seqf1olem2  11086  seqf1o  11087  ccatfn  11427  limsuple  11952  limsuplt  11953  limsupbnd1  11956  caucvgrlem  12145  prdsval  13355  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsds  13363  prdshom  13366  plusffval  14379  gsumval  14452  frmdplusg  14476  vrmdfval  14478  odinf  14876  efgtf  15031  gsumval3  15191  staffval  15612  scaffval  15645  cnfldcj  16386  cnfldds  16389  xrsadd  16391  xrsmul  16392  xrsds  16414  ipffval  16552  ocvfval  16566  cnpfval  16964  iscnp2  16969  txcn  17320  fmval  17638  fmf  17640  tsmsval  17813  tsmsadd  17829  blfval  17947  nmfval  18111  tngnm  18167  tngngp2  18168  tngngpd  18169  tngngp  18170  nmoffn  18220  nmofval  18223  ishtpy  18470  tchex  18649  adjeu  22469  ismeas  23530  nZdef  25180  isismty  26525  rrnval  26551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696  df-cnv 4697  df-dm 4699  df-rn 4700  df-fun 5257  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator