Theorem fex2 7958

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951   × cxp 5683  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  elmapg  8879  f1oen2g  9009  f1dom2g  9010  dom3d  9034  domssex2  9177  domssex  9178  mapxpen  9183  oismo  9580  wdomima2g  9626  dfac8clem  10072  acni2  10086  acnlem  10088  dfac4  10162  dfac2a  10170  axdc2lem  10488  axdc4lem  10495  axcclem  10497  mpoaddex  13030  addex  13031  mpomulex  13032  mulex  13033  seqf1olem2  14083  seqf1o  14084  limsuple  15514  limsuplt  15515  limsupbnd1  15518  caucvgrlem  15709  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  gsumval  18690  frmdplusg  18867  isghm  19233  odinf  19581  staffval  20842  cnfldcj  21373  cnfldds  21376  cnfldcjOLD  21386  cnflddsOLD  21389  xrsadd  21397  xrsmul  21398  xrsds  21427  ocvfval  21684  cnpfval  23242  iscnp2  23247  fmf  23953  tsmsval  24139  blfvalps  24393  nmfval  24601  tngnm  24672  tngngp2  24673  tngngpd  24674  tngngp  24675  nmoffn  24732  nmofval  24735  ishtpy  25004  tcphex  25251  elno  27690  adjeu  31908  ismeas  34200  isismty  37808  rrnval  37834  subex  42288  absex  42289  cjex  42290  sn-isghm  42683