Theorem fex2 7917

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7733	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1143	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6719	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1146	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5280	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1098   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904   × cxp 5645  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-cnv 5655  df-dm 5657  df-rn 5658  df-fun 6523  df-fn 6524  df-f 6525

This theorem is referenced by:  elmapg  8820  f1oen2g  8949  f1dom2g  8950  dom3d  8975  domssex2  9109  domssex  9110  mapxpen  9115  oismo  9488  wdomima2g  9534  dfac8clem  9988  acni2  10002  acnlem  10004  dfac4  10078  dfac2a  10086  axdc2lem  10405  axdc4lem  10412  axcclem  10414  mpoaddex  12989  addex  12990  mpomulex  12991  mulex  12992  seqf1olem2  14055  seqf1o  14056  limsuple  15505  limsuplt  15506  limsupbnd1  15509  caucvgrlem  15700  prdsplusg  17487  prdsmulr  17488  prdsvsca  17489  prdshom  17496  gsumval  18711  frmdplusg  18888  isghm  19256  odinf  19603  staffval  20887  cnfldcj  21430  cnfldds  21433  xrsadd  21439  xrsmul  21440  xrsds  21459  ocvfval  21715  cnpfval  23291  iscnp2  23296  fmf  24002  tsmsval  24188  blfvalps  24440  nmfval  24645  tngnm  24708  tngngp2  24709  tngngpd  24710  tngngp  24711  nmoffn  24768  nmofval  24771  ishtpy  25031  tcphex  25276  elno  27707  adjeu  32089  ismeas  34493  isismty  38297  rrnval  38323  subex  42860  absex  42861  cjex  42862  sn-isghm  43252