Theorem fex2 7121

Description: A function with bounded domain and range is a set. This version of fex 6490 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)

Assertion

Ref	Expression
fex2	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 6960	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1079	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6060	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1082	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 4805	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1037   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574   × cxp 5112  ⟶wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  elmapg  7870  f1oen2g  7972  f1dom2g  7973  dom3d  7997  domssex2  8120  domssex  8121  mapxpen  8126  oismo  8445  wdomima2g  8491  ixpiunwdom  8496  dfac8clem  8855  ac5num  8859  acni2  8869  acnlem  8871  dfac4  8945  dfac2a  8952  axdc2lem  9270  axdc4lem  9277  axcclem  9279  ac6num  9301  axdclem2  9342  addex  11830  mulex  11831  seqf1olem2  12841  seqf1o  12842  hasheqf1oiOLD  13141  limsuple  14209  limsuplt  14210  limsupbnd1  14213  caucvgrlem  14403  prdsval  16115  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdsds  16124  prdshom  16127  plusffval  17247  gsumval  17271  frmdplusg  17391  vrmdfval  17393  odinf  17980  efgtf  18135  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  staffval  18847  scaffval  18881  cnfldcj  19753  cnfldds  19756  xrsadd  19763  xrsmul  19764  xrsds  19789  ipffval  19993  ocvfval  20010  cnpfval  21038  iscnp2  21043  txcn  21429  fmval  21747  fmf  21749  tsmsval  21934  tsmsadd  21950  blfvalps  22188  nmfval  22393  tngnm  22455  tngngp2  22456  tngngpd  22457  tngngp  22458  nmoffn  22515  nmofval  22518  ishtpy  22771  tchex  23016  adjeu  28748  ismeas  30262  hgt750lemg  30732  isismty  33600  rrnval  33626