Theorem fex2 7287

Description: A function with bounded domain and range is a set. This version of fex 6654 is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7126	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1125	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6221	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1128	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 4957	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1072   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715   × cxp 5264  ⟶wf 6045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-rel 5273  df-cnv 5274  df-dm 5276  df-rn 5277  df-fun 6051  df-fn 6052  df-f 6053

This theorem is referenced by:  elmapg  8038  f1oen2g  8140  f1dom2g  8141  dom3d  8165  domssex2  8287  domssex  8288  mapxpen  8293  oismo  8612  wdomima2g  8658  ixpiunwdom  8663  dfac8clem  9065  ac5num  9069  acni2  9079  acnlem  9081  dfac4  9155  dfac2a  9162  axdc2lem  9482  axdc4lem  9489  axcclem  9491  ac6num  9513  axdclem2  9554  addex  12043  mulex  12044  seqf1olem2  13055  seqf1o  13056  limsuple  14428  limsuplt  14429  limsupbnd1  14432  caucvgrlem  14622  prdsval  16337  prdsplusg  16340  prdsmulr  16341  prdsvsca  16342  prdsds  16346  prdshom  16349  plusffval  17468  gsumval  17492  frmdplusg  17612  vrmdfval  17614  odinf  18200  efgtf  18355  gsumval3lem1  18526  gsumval3lem2  18527  gsumval3  18528  staffval  19069  scaffval  19103  cnfldcj  19975  cnfldds  19978  xrsadd  19985  xrsmul  19986  xrsds  20011  ipffval  20215  ocvfval  20232  cnpfval  21260  iscnp2  21265  txcn  21651  fmval  21968  fmf  21970  tsmsval  22155  tsmsadd  22171  blfvalps  22409  nmfval  22614  tngnm  22676  tngngp2  22677  tngngpd  22678  tngngp  22679  nmoffn  22736  nmofval  22739  ishtpy  22992  tchex  23236  adjeu  29078  ismeas  30592  hgt750lemg  31062  isismty  33931  rrnval  33957