Theorem fex2 7901

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7715	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1130	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6727	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1133	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5312	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2106  Vcvv 3469   ⊆ wss 3939   × cxp 5662  ⟶wf 6523

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5287  ax-nul 5294  ax-pow 5351  ax-pr 5415  ax-un 7703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3429  df-v 3471  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4314  df-if 4518  df-pw 4593  df-sn 4618  df-pr 4620  df-op 4624  df-uni 4897  df-br 5137  df-opab 5199  df-xp 5670  df-rel 5671  df-cnv 5672  df-dm 5674  df-rn 5675  df-fun 6529  df-fn 6530  df-f 6531

This theorem is referenced by:  elmapg  8811  f1oen2g  8942  f1dom2g  8943  f1dom2gOLD  8944  dom3d  8968  domssex2  9115  domssex  9116  mapxpen  9121  oismo  9512  wdomima2g  9558  dfac8clem  10004  acni2  10018  acnlem  10020  dfac4  10094  dfac2a  10101  axdc2lem  10420  axdc4lem  10427  axcclem  10429  addex  12949  mulex  12950  seqf1olem2  13985  seqf1o  13986  limsuple  15399  limsuplt  15400  limsupbnd1  15403  caucvgrlem  15596  prdsplusg  17381  prdsmulr  17382  prdsvsca  17383  prdshom  17390  gsumval  18573  frmdplusg  18705  odinf  19390  staffval  20397  cnfldcj  20878  cnfldds  20881  xrsadd  20889  xrsmul  20890  xrsds  20915  ocvfval  21145  cnpfval  22660  iscnp2  22665  fmf  23371  tsmsval  23557  blfvalps  23811  nmfval  24019  tngnm  24090  tngngp2  24091  tngngpd  24092  tngngp  24093  nmoffn  24150  nmofval  24153  ishtpy  24410  tcphex  24656  adjeu  30951  ismeas  32963  isismty  36409  rrnval  36435