Theorem fex2 7887

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889   × cxp 5629  ⟶wf 6494

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 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  elmapg  8786  f1oen2g  8915  f1dom2g  8916  dom3d  8941  domssex2  9075  domssex  9076  mapxpen  9081  oismo  9455  wdomima2g  9501  dfac8clem  9954  acni2  9968  acnlem  9970  dfac4  10044  dfac2a  10052  axdc2lem  10370  axdc4lem  10377  axcclem  10379  mpoaddex  12938  addex  12939  mpomulex  12940  mulex  12941  seqf1olem2  14004  seqf1o  14005  limsuple  15440  limsuplt  15441  limsupbnd1  15444  caucvgrlem  15635  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  gsumval  18645  frmdplusg  18822  isghm  19190  odinf  19538  staffval  20818  cnfldcj  21361  cnfldds  21364  xrsadd  21370  xrsmul  21371  xrsds  21390  ocvfval  21646  cnpfval  23199  iscnp2  23204  fmf  23910  tsmsval  24096  blfvalps  24348  nmfval  24553  tngnm  24616  tngngp2  24617  tngngpd  24618  tngngp  24619  nmoffn  24676  nmofval  24679  ishtpy  24939  tcphex  25184  elno  27609  adjeu  31960  ismeas  34343  isismty  38122  rrnval  38148  subex  42686  absex  42687  cjex  42688  sn-isghm  43106