Theorem fex2 7881

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   × cxp 5623  ⟶wf 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  elmapg  8780  f1oen2g  8909  f1dom2g  8910  dom3d  8935  domssex2  9069  domssex  9070  mapxpen  9075  oismo  9449  wdomima2g  9495  dfac8clem  9948  acni2  9962  acnlem  9964  dfac4  10038  dfac2a  10046  axdc2lem  10364  axdc4lem  10371  axcclem  10373  mpoaddex  12932  addex  12933  mpomulex  12934  mulex  12935  seqf1olem2  13998  seqf1o  13999  limsuple  15434  limsuplt  15435  limsupbnd1  15438  caucvgrlem  15629  prdsplusg  17415  prdsmulr  17416  prdsvsca  17417  prdshom  17424  gsumval  18639  frmdplusg  18816  isghm  19184  odinf  19532  staffval  20812  cnfldcj  21356  cnfldds  21359  cnfldcjOLD  21369  cnflddsOLD  21372  xrsadd  21378  xrsmul  21379  xrsds  21402  ocvfval  21659  cnpfval  23212  iscnp2  23217  fmf  23923  tsmsval  24109  blfvalps  24361  nmfval  24566  tngnm  24629  tngngp2  24630  tngngpd  24631  tngngp  24632  nmoffn  24689  nmofval  24692  ishtpy  24952  tcphex  25197  elno  27626  adjeu  31978  ismeas  34362  isismty  38139  rrnval  38165  subex  42703  absex  42704  cjex  42705  sn-isghm  43123