Theorem fex2 7939

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

Assertion

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

Proof of Theorem fex2

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2146  Vcvv 3457   ⊆ wss 3906   × cxp 5661  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  elmapg  8842  f1oen2g  8971  f1dom2g  8972  dom3d  8997  domssex2  9132  domssex  9133  mapxpen  9138  oismo  9509  wdomima2g  9555  dfac8clem  10032  acni2  10046  acnlem  10048  dfac4  10122  dfac2a  10129  axdc2lem  10447  axdc4lem  10454  axcclem  10456  mpoaddex  13028  addex  13029  mpomulex  13030  mulex  13031  seqf1olem2  14096  seqf1o  14097  limsuple  15553  limsuplt  15554  limsupbnd1  15557  caucvgrlem  15748  prdsplusg  17533  prdsmulr  17534  prdsvsca  17535  prdshom  17542  gsumval  18767  frmdplusg  18950  isghm  19330  odinf  19677  staffval  20994  cnfldcj  21581  cnfldds  21584  xrsadd  21590  xrsmul  21591  xrsds  21610  ocvfval  21866  cnpfval  23441  iscnp2  23446  fmf  24153  tsmsval  24339  blfvalps  24591  nmfval  24796  tngnm  24859  tngngp2  24860  tngngpd  24861  tngngp  24862  nmoffn  24919  nmofval  24922  ishtpy  25182  tcphex  25427  elno  27861  adjeu  32312  ismeas  34654  isismty  38510  rrnval  38536  subex  43073  absex  43074  cjex  43075  sn-isghm  43463