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

Theorem fex2 7629
Description: A function with bounded domain and range is a set. This version of fex 6987 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
fex2 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)

Proof of Theorem fex2
StepHypRef Expression
1 xpexg 7465 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
213adant1 1124 . 2 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
3 fssxp 6530 . . 3 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
433ad2ant1 1127 . 2 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
52, 4ssexd 5224 1 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081  wcel 2107  Vcvv 3499  wss 3939   × cxp 5551  wf 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-xp 5559  df-rel 5560  df-cnv 5561  df-dm 5563  df-rn 5564  df-fun 6353  df-fn 6354  df-f 6355
This theorem is referenced by:  elmapg  8412  f1oen2g  8518  f1dom2g  8519  dom3d  8543  domssex2  8669  domssex  8670  mapxpen  8675  oismo  8996  wdomima2g  9042  ixpiunwdom  9047  dfac8clem  9450  acni2  9464  acnlem  9466  dfac4  9540  dfac2a  9547  axdc2lem  9862  axdc4lem  9869  axcclem  9871  axdclem2  9934  addex  12380  mulex  12381  seqf1olem2  13403  seqf1o  13404  limsuple  14828  limsuplt  14829  limsupbnd1  14832  caucvgrlem  15022  prdsval  16720  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdsds  16729  prdshom  16732  plusffval  17849  gsumval  17878  frmdplusg  18004  odinf  18612  efgtf  18770  gsumval3lem1  18947  gsumval3lem2  18948  gsumval3  18949  staffval  19540  scaffval  19574  cnfldcj  20468  cnfldds  20471  xrsadd  20478  xrsmul  20479  xrsds  20504  ipffval  20708  ocvfval  20726  cnpfval  21758  iscnp2  21763  txcn  22150  fmval  22467  fmf  22469  tsmsval  22654  tsmsadd  22670  blfvalps  22908  nmfval  23113  tngnm  23175  tngngp2  23176  tngngpd  23177  tngngp  23178  nmoffn  23235  nmofval  23238  ishtpy  23491  tcphex  23735  adjeu  29580  ismeas  31344  hgt750lemg  31811  isismty  34947  rrnval  34973
  Copyright terms: Public domain W3C validator