Theorem fex2 7952

Description: A function with bounded domain and codomain is a set. This version of fex 7236 is proven without the Axiom of Replacement ax-rep 5231, but depends on ax-un 7755, which is not required for the proof of fex 7236. (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 1148	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6742	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1151	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5286	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3896   × cxp 5649  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  elmapg  8867  f1oen2g  9003  f1dom2g  9004  dom3d  9029  domssex2  9164  domssex  9165  mapxpen  9170  oismo  9541  wdomima2g  9587  dfac8clem  10118  acni2  10132  acnlem  10134  dfac4  10208  dfac2a  10215  axdc2lem  10533  axdc4lem  10540  axcclem  10542  mpoaddex  13123  addex  13124  mpomulex  13125  mulex  13126  seqf1olem2  14192  seqf1o  14193  limsuple  15654  limsuplt  15655  limsupbnd1  15658  caucvgrlem  15849  prdsplusg  17638  prdsmulr  17639  prdsvsca  17640  prdshom  17647  gsumval  18875  frmdplusg  19059  isghm  19439  odinf  19786  staffval  21107  cnfldcj  21696  cnfldds  21699  xrsadd  21705  xrsmul  21706  xrsds  21725  ocvfval  21981  cnpfval  23561  iscnp2  23566  fmf  24273  tsmsval  24459  blfvalps  24711  nmfval  24916  tngnm  24979  tngngp2  24980  tngngpd  24981  tngngp  24982  nmoffn  25039  nmofval  25042  ishtpy  25302  tcphex  25547  elno  28012  adjeu  32500  ismeas  34882  isismty  38872  rrnval  38898  subex  43435  absex  43436  cjex  43437  sn-isghm  43821