Theorem fex2 7649

Description: A function with bounded domain and range is a set. This version of fex 6986 is proven without the Axiom of Replacement ax-rep 5160, but depends on ax-un 7465, which is not required for the proof of fex 6986. (Contributed by Mario Carneiro, 24-Jun-2015.)

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7477	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1127	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6524	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1130	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5198	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111  Vcvv 3409   ⊆ wss 3860   × cxp 5526  ⟶wf 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-xp 5534  df-rel 5535  df-cnv 5536  df-dm 5538  df-rn 5539  df-fun 6342  df-fn 6343  df-f 6344

This theorem is referenced by:  elmapg  8435  f1oen2g  8557  f1dom2g  8558  dom3d  8582  domssex2  8712  domssex  8713  mapxpen  8718  oismo  9050  wdomima2g  9096  ixpiunwdom  9100  dfac8clem  9505  acni2  9519  acnlem  9521  dfac4  9595  dfac2a  9602  axdc2lem  9921  axdc4lem  9928  axcclem  9930  addex  12441  mulex  12442  seqf1olem2  13473  seqf1o  13474  limsuple  14896  limsuplt  14897  limsupbnd1  14900  caucvgrlem  15090  prdsval  16799  prdsplusg  16802  prdsmulr  16803  prdsvsca  16804  prdshom  16811  gsumval  17966  frmdplusg  18098  odinf  18770  efgtf  18928  gsumval3lem1  19106  gsumval3  19108  staffval  19699  cnfldcj  20186  cnfldds  20189  xrsadd  20196  xrsmul  20197  xrsds  20222  ocvfval  20444  cnpfval  21947  iscnp2  21952  txcn  22339  fmval  22656  fmf  22658  tsmsval  22844  tsmsadd  22860  blfvalps  23098  nmfval  23303  tngnm  23366  tngngp2  23367  tngngpd  23368  tngngp  23369  nmoffn  23426  nmofval  23429  ishtpy  23686  tcphex  23930  adjeu  29784  ismeas  31698  hgt750lemg  32165  isismty  35553  rrnval  35579