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

Theorem fex2 6739
Description: A function with bounded domain and range is a set. This version of fex 6126 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 6584 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
213adant1 1015 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  ( A  X.  B
)  e.  _V )
3 fssxp 5726 . . 3  |-  ( F : A --> B  ->  F  C_  ( A  X.  B ) )
433ad2ant1 1018 . 2  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  C_  ( A  X.  B ) )
52, 4ssexd 4541 1  |-  ( ( F : A --> B  /\  A  e.  V  /\  B  e.  W )  ->  F  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974    e. wcel 1842   _Vcvv 3059    C_ wss 3414    X. cxp 4821   -->wf 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-xp 4829  df-rel 4830  df-cnv 4831  df-dm 4833  df-rn 4834  df-fun 5571  df-fn 5572  df-f 5573
This theorem is referenced by:  elmapg  7470  f1oen2g  7570  f1dom2g  7571  dom3d  7595  domssex2  7715  domssex  7716  mapxpen  7721  oismo  7999  wdomima2g  8046  ixpiunwdom  8051  dfac8clem  8445  ac5num  8449  acni2  8459  acnlem  8461  dfac4  8535  dfac2a  8542  axdc2lem  8860  axdc4lem  8867  axcclem  8869  ac6num  8891  axdclem2  8932  addex  11263  mulex  11264  seqf1olem2  12191  seqf1o  12192  hasheqf1oi  12471  ccatfnOLD  12645  limsuple  13450  limsuplt  13451  limsupbnd1  13454  caucvgrlem  13644  prdsval  15069  prdsplusg  15072  prdsmulr  15073  prdsvsca  15074  prdsds  15078  prdshom  15081  plusffval  16201  gsumval  16222  frmdplusg  16346  vrmdfval  16348  odinf  16909  efgtf  17064  gsumval3OLD  17232  gsumval3lem1  17233  gsumval3lem2  17234  gsumval3  17235  staffval  17816  scaffval  17850  cnfldcj  18747  cnfldds  18750  xrsadd  18755  xrsmul  18756  xrsds  18781  ipffval  18981  ocvfval  18995  cnpfval  20028  iscnp2  20033  txcn  20419  fmval  20736  fmf  20738  tsmsval  20921  tsmsadd  20941  blfvalps  21178  nmfval  21401  tngnm  21457  tngngp2  21458  tngngpd  21459  tngngp  21460  nmoffn  21510  nmofval  21513  ishtpy  21764  tchex  21952  adjeu  27221  ismeas  28647  isismty  31579  rrnval  31605
  Copyright terms: Public domain W3C validator