Theorem fex2 7956

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962   × cxp 5686  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  elmapg  8877  f1oen2g  9007  f1dom2g  9008  dom3d  9032  domssex2  9175  domssex  9176  mapxpen  9181  oismo  9577  wdomima2g  9623  dfac8clem  10069  acni2  10083  acnlem  10085  dfac4  10159  dfac2a  10167  axdc2lem  10485  axdc4lem  10492  axcclem  10494  mpoaddex  13027  addex  13028  mpomulex  13029  mulex  13030  seqf1olem2  14079  seqf1o  14080  limsuple  15510  limsuplt  15511  limsupbnd1  15514  caucvgrlem  15705  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  gsumval  18702  frmdplusg  18879  isghm  19245  odinf  19595  staffval  20858  cnfldcj  21390  cnfldds  21393  cnfldcjOLD  21403  cnflddsOLD  21406  xrsadd  21414  xrsmul  21415  xrsds  21444  ocvfval  21701  cnpfval  23257  iscnp2  23262  fmf  23968  tsmsval  24154  blfvalps  24408  nmfval  24616  tngnm  24687  tngngp2  24688  tngngpd  24689  tngngp  24690  nmoffn  24747  nmofval  24750  ishtpy  25017  tcphex  25264  elno  27704  adjeu  31917  ismeas  34179  isismty  37787  rrnval  37813  subex  42266  absex  42267  cjex  42268  sn-isghm  42659