Theorem fex2 7929

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1103   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905   × cxp 5659  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-dm 5671  df-rn 5672  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  elmapg  8832  f1oen2g  8961  f1dom2g  8962  dom3d  8987  domssex2  9121  domssex  9122  mapxpen  9127  oismo  9498  wdomima2g  9544  dfac8clem  10012  acni2  10026  acnlem  10028  dfac4  10102  dfac2a  10109  axdc2lem  10427  axdc4lem  10434  axcclem  10436  mpoaddex  13007  addex  13008  mpomulex  13009  mulex  13010  seqf1olem2  14074  seqf1o  14075  limsuple  15525  limsuplt  15526  limsupbnd1  15529  caucvgrlem  15720  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  prdshom  17515  gsumval  18730  frmdplusg  18908  isghm  19281  odinf  19628  staffval  20944  cnfldcj  21531  cnfldds  21534  xrsadd  21540  xrsmul  21541  xrsds  21560  ocvfval  21816  cnpfval  23391  iscnp2  23396  fmf  24102  tsmsval  24288  blfvalps  24540  nmfval  24745  tngnm  24808  tngngp2  24809  tngngpd  24810  tngngp  24811  nmoffn  24868  nmofval  24871  ishtpy  25131  tcphex  25376  elno  27810  adjeu  32241  ismeas  34589  isismty  38452  rrnval  38478  subex  43015  absex  43016  cjex  43017  sn-isghm  43405