Theorem fex2 7926

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948   × cxp 5674  ⟶wf 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  elmapg  8835  f1oen2g  8966  f1dom2g  8967  f1dom2gOLD  8968  dom3d  8992  domssex2  9139  domssex  9140  mapxpen  9145  oismo  9537  wdomima2g  9583  dfac8clem  10029  acni2  10043  acnlem  10045  dfac4  10119  dfac2a  10126  axdc2lem  10445  axdc4lem  10452  axcclem  10454  addex  12974  mulex  12975  seqf1olem2  14010  seqf1o  14011  limsuple  15424  limsuplt  15425  limsupbnd1  15428  caucvgrlem  15621  prdsplusg  17406  prdsmulr  17407  prdsvsca  17408  prdshom  17415  gsumval  18598  frmdplusg  18737  odinf  19433  staffval  20459  cnfldcj  20957  cnfldds  20960  xrsadd  20968  xrsmul  20969  xrsds  20994  ocvfval  21225  cnpfval  22745  iscnp2  22750  fmf  23456  tsmsval  23642  blfvalps  23896  nmfval  24104  tngnm  24175  tngngp2  24176  tngngpd  24177  tngngp  24178  nmoffn  24235  nmofval  24238  ishtpy  24495  tcphex  24741  adjeu  31180  ismeas  33266  mpomulex  35236  mpoaddex  35261  gg-cnfldcj  35267  gg-cnfldds  35270  isismty  36761  rrnval  36787