Theorem fex2 7915

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917   × cxp 5639  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  elmapg  8815  f1oen2g  8943  f1dom2g  8944  dom3d  8968  domssex2  9107  domssex  9108  mapxpen  9113  oismo  9500  wdomima2g  9546  dfac8clem  9992  acni2  10006  acnlem  10008  dfac4  10082  dfac2a  10090  axdc2lem  10408  axdc4lem  10415  axcclem  10417  mpoaddex  12954  addex  12955  mpomulex  12956  mulex  12957  seqf1olem2  14014  seqf1o  14015  limsuple  15451  limsuplt  15452  limsupbnd1  15455  caucvgrlem  15646  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  gsumval  18611  frmdplusg  18788  isghm  19154  odinf  19500  staffval  20757  cnfldcj  21280  cnfldds  21283  cnfldcjOLD  21293  cnflddsOLD  21296  xrsadd  21303  xrsmul  21304  xrsds  21333  ocvfval  21582  cnpfval  23128  iscnp2  23133  fmf  23839  tsmsval  24025  blfvalps  24278  nmfval  24483  tngnm  24546  tngngp2  24547  tngngpd  24548  tngngp  24549  nmoffn  24606  nmofval  24609  ishtpy  24878  tcphex  25124  elno  27564  adjeu  31825  ismeas  34196  isismty  37802  rrnval  37828  subex  42242  absex  42243  cjex  42244  sn-isghm  42668