Theorem fex2 7640

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

Syntax hints:   → wi 4   ∧ w3a 1083   ∈ wcel 2114  Vcvv 3496   ⊆ wss 3938   × cxp 5555  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-cnv 5565  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  elmapg  8421  f1oen2g  8528  f1dom2g  8529  dom3d  8553  domssex2  8679  domssex  8680  mapxpen  8685  oismo  9006  wdomima2g  9052  ixpiunwdom  9057  dfac8clem  9460  acni2  9474  acnlem  9476  dfac4  9550  dfac2a  9557  axdc2lem  9872  axdc4lem  9879  axcclem  9881  axdclem2  9944  addex  12390  mulex  12391  seqf1olem2  13413  seqf1o  13414  limsuple  14837  limsuplt  14838  limsupbnd1  14841  caucvgrlem  15031  prdsval  16730  prdsplusg  16733  prdsmulr  16734  prdsvsca  16735  prdsds  16739  prdshom  16742  gsumval  17889  frmdplusg  18021  odinf  18692  efgtf  18850  gsumval3lem1  19027  gsumval3lem2  19028  gsumval3  19029  staffval  19620  cnfldcj  20554  cnfldds  20557  xrsadd  20564  xrsmul  20565  xrsds  20590  ocvfval  20812  cnpfval  21844  iscnp2  21849  txcn  22236  fmval  22553  fmf  22555  tsmsval  22741  tsmsadd  22757  blfvalps  22995  nmfval  23200  tngnm  23262  tngngp2  23263  tngngpd  23264  tngngp  23265  nmoffn  23322  nmofval  23325  ishtpy  23578  tcphex  23822  adjeu  29668  ismeas  31460  hgt750lemg  31927  isismty  35081  rrnval  35107