Theorem fex2 7880

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7697	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1131	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6689	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1134	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5261	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   × cxp 5622  ⟶wf 6488

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  elmapg  8779  f1oen2g  8908  f1dom2g  8909  dom3d  8934  domssex2  9068  domssex  9069  mapxpen  9074  oismo  9448  wdomima2g  9494  dfac8clem  9945  acni2  9959  acnlem  9961  dfac4  10035  dfac2a  10043  axdc2lem  10361  axdc4lem  10368  axcclem  10370  mpoaddex  12929  addex  12930  mpomulex  12931  mulex  12932  seqf1olem2  13995  seqf1o  13996  limsuple  15431  limsuplt  15432  limsupbnd1  15435  caucvgrlem  15626  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  gsumval  18636  frmdplusg  18813  isghm  19181  odinf  19529  staffval  20809  cnfldcj  21353  cnfldds  21356  cnfldcjOLD  21366  cnflddsOLD  21369  xrsadd  21375  xrsmul  21376  xrsds  21399  ocvfval  21656  cnpfval  23209  iscnp2  23214  fmf  23920  tsmsval  24106  blfvalps  24358  nmfval  24563  tngnm  24626  tngngp2  24627  tngngpd  24628  tngngp  24629  nmoffn  24686  nmofval  24689  ishtpy  24949  tcphex  25194  elno  27623  adjeu  31975  ismeas  34359  isismty  38136  rrnval  38162  subex  42700  absex  42701  cjex  42702  sn-isghm  43120