Theorem fex2 7934

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7750	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1148	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6731	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1151	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5289	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3899   × cxp 5653  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537

This theorem is used by:  elmapg  8839  f1oen2g  8975  f1dom2g  8976  dom3d  9001  domssex2  9136  domssex  9137  mapxpen  9142  oismo  9513  wdomima2g  9559  dfac8clem  10036  acni2  10050  acnlem  10052  dfac4  10126  dfac2a  10133  axdc2lem  10451  axdc4lem  10458  axcclem  10460  mpoaddex  13039  addex  13040  mpomulex  13041  mulex  13042  seqf1olem2  14107  seqf1o  14108  limsuple  15566  limsuplt  15567  limsupbnd1  15570  caucvgrlem  15761  prdsplusg  17544  prdsmulr  17545  prdsvsca  17546  prdshom  17553  gsumval  18780  frmdplusg  18964  isghm  19344  odinf  19691  staffval  21008  cnfldcj  21595  cnfldds  21598  xrsadd  21604  xrsmul  21605  xrsds  21624  ocvfval  21880  cnpfval  23460  iscnp2  23465  fmf  24172  tsmsval  24358  blfvalps  24610  nmfval  24815  tngnm  24878  tngngp2  24879  tngngpd  24880  tngngp  24881  nmoffn  24938  nmofval  24941  ishtpy  25201  tcphex  25446  elno  27883  adjeu  32371  ismeas  34711  isismty  38552  rrnval  38578  subex  43115  absex  43116  cjex  43117  sn-isghm  43520