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

Theorem fex2 7068
Description: A function with bounded domain and range is a set. This version of fex 6444 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 6913 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
213adant1 1077 . 2 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
3 fssxp 6017 . . 3 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
433ad2ant1 1080 . 2 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
52, 4ssexd 4765 1 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036  wcel 1987  Vcvv 3186  wss 3555   × cxp 5072  wf 5843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-xp 5080  df-rel 5081  df-cnv 5082  df-dm 5084  df-rn 5085  df-fun 5849  df-fn 5850  df-f 5851
This theorem is referenced by:  elmapg  7815  f1oen2g  7916  f1dom2g  7917  dom3d  7941  domssex2  8064  domssex  8065  mapxpen  8070  oismo  8389  wdomima2g  8435  ixpiunwdom  8440  dfac8clem  8799  ac5num  8803  acni2  8813  acnlem  8815  dfac4  8889  dfac2a  8896  axdc2lem  9214  axdc4lem  9221  axcclem  9223  ac6num  9245  axdclem2  9286  addex  11774  mulex  11775  seqf1olem2  12781  seqf1o  12782  hasheqf1oiOLD  13081  limsuple  14143  limsuplt  14144  limsupbnd1  14147  caucvgrlem  14337  prdsval  16036  prdsplusg  16039  prdsmulr  16040  prdsvsca  16041  prdsds  16045  prdshom  16048  plusffval  17168  gsumval  17192  frmdplusg  17312  vrmdfval  17314  odinf  17901  efgtf  18056  gsumval3lem1  18227  gsumval3lem2  18228  gsumval3  18229  staffval  18768  scaffval  18802  cnfldcj  19672  cnfldds  19675  xrsadd  19682  xrsmul  19683  xrsds  19708  ipffval  19912  ocvfval  19929  cnpfval  20948  iscnp2  20953  txcn  21339  fmval  21657  fmf  21659  tsmsval  21844  tsmsadd  21860  blfvalps  22098  nmfval  22303  tngnm  22365  tngngp2  22366  tngngpd  22367  tngngp  22368  nmoffn  22425  nmofval  22428  ishtpy  22679  tchex  22924  adjeu  28594  ismeas  30040  isismty  33229  rrnval  33255
  Copyright terms: Public domain W3C validator