Theorem fex2 7876

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2113  Vcvv 3438   ⊆ wss 3899   × cxp 5620  ⟶wf 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-cnv 5630  df-dm 5632  df-rn 5633  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  elmapg  8774  f1oen2g  8903  f1dom2g  8904  dom3d  8929  domssex2  9063  domssex  9064  mapxpen  9069  oismo  9443  wdomima2g  9489  dfac8clem  9940  acni2  9954  acnlem  9956  dfac4  10030  dfac2a  10038  axdc2lem  10356  axdc4lem  10363  axcclem  10365  mpoaddex  12899  addex  12900  mpomulex  12901  mulex  12902  seqf1olem2  13963  seqf1o  13964  limsuple  15399  limsuplt  15400  limsupbnd1  15403  caucvgrlem  15594  prdsplusg  17376  prdsmulr  17377  prdsvsca  17378  prdshom  17385  gsumval  18600  frmdplusg  18777  isghm  19142  odinf  19490  staffval  20772  cnfldcj  21316  cnfldds  21319  cnfldcjOLD  21329  cnflddsOLD  21332  xrsadd  21338  xrsmul  21339  xrsds  21362  ocvfval  21619  cnpfval  23176  iscnp2  23181  fmf  23887  tsmsval  24073  blfvalps  24325  nmfval  24530  tngnm  24593  tngngp2  24594  tngngpd  24595  tngngp  24596  nmoffn  24653  nmofval  24656  ishtpy  24925  tcphex  25171  elno  27611  adjeu  31913  ismeas  34305  isismty  37941  rrnval  37967  subex  42444  absex  42445  cjex  42446  sn-isghm  42858