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

Theorem fex2 6521
Description: A function with bounded domain and range is a set. This version of fex 5937 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 xpexg 6496 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
213adant1 999 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
3 fssxp 5558 . . 3  |-  ( F : A --> B  ->  F  C_  ( A  X.  B ) )
433ad2ant1 1002 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  C_  ( A  X.  B ) )
52, 4ssexd 4427 1  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958    e. wcel 1755   _Vcvv 2962    C_ wss 3316    X. cxp 4825   -->wf 5402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-xp 4833  df-rel 4834  df-cnv 4835  df-dm 4837  df-rn 4838  df-fun 5408  df-fn 5409  df-f 5410
This theorem is referenced by:  elmapg  7215  f1oen2g  7314  f1dom2g  7315  dom3d  7339  domssex2  7459  domssex  7460  mapxpen  7465  oismo  7742  wdomima2g  7789  ixpiunwdom  7794  dfac8clem  8190  ac5num  8194  acni2  8204  acnlem  8206  dfac4  8280  dfac2a  8287  axdc2lem  8605  axdc4lem  8612  axcclem  8614  ac6num  8636  axdclem2  8677  addex  10976  mulex  10977  seqf1olem2  11829  seqf1o  11830  hasheqf1oi  12105  ccatfn  12255  limsuple  12939  limsuplt  12940  limsupbnd1  12943  caucvgrlem  13133  prdsval  14375  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdsds  14384  prdshom  14387  plusffval  15409  gsumval  15484  frmdplusg  15511  vrmdfval  15513  odinf  16043  efgtf  16198  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3lem2  16363  gsumval3  16364  staffval  16855  scaffval  16889  cnfldcj  17668  cnfldds  17671  xrsadd  17676  xrsmul  17677  xrsds  17699  ipffval  17918  ocvfval  17932  cnpfval  18679  iscnp2  18684  txcn  19040  fmval  19357  fmf  19359  tsmsval  19542  tsmsadd  19562  blfvalps  19799  nmfval  20022  tngnm  20078  tngngp2  20079  tngngpd  20080  tngngp  20081  nmoffn  20131  nmofval  20134  ishtpy  20385  tchex  20573  adjeu  25115  ismeas  26466  isismty  28541  rrnval  28567
  Copyright terms: Public domain W3C validator