Theorem fex2 7620

Description: A function with bounded domain and range is a set. This version of fex 6966 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 7453	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1127	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6508	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1130	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5192	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881   × cxp 5517  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  elmapg  8402  f1oen2g  8509  f1dom2g  8510  dom3d  8534  domssex2  8661  domssex  8662  mapxpen  8667  oismo  8988  wdomima2g  9034  ixpiunwdom  9038  dfac8clem  9443  acni2  9457  acnlem  9459  dfac4  9533  dfac2a  9540  axdc2lem  9859  axdc4lem  9866  axcclem  9868  axdclem2  9931  addex  12375  mulex  12376  seqf1olem2  13406  seqf1o  13407  limsuple  14827  limsuplt  14828  limsupbnd1  14831  caucvgrlem  15021  prdsval  16720  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdshom  16732  gsumval  17879  frmdplusg  18011  odinf  18682  efgtf  18840  gsumval3lem1  19018  gsumval3lem2  19019  gsumval3  19020  staffval  19611  cnfldcj  20098  cnfldds  20101  xrsadd  20108  xrsmul  20109  xrsds  20134  ocvfval  20355  cnpfval  21839  iscnp2  21844  txcn  22231  fmval  22548  fmf  22550  tsmsval  22736  tsmsadd  22752  blfvalps  22990  nmfval  23195  tngnm  23257  tngngp2  23258  tngngpd  23259  tngngp  23260  nmoffn  23317  nmofval  23320  ishtpy  23577  tcphex  23821  adjeu  29672  ismeas  31568  hgt750lemg  32035  isismty  35239  rrnval  35265