Theorem fex2 7641

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

Syntax hints:   → wi 4   ∧ w3a 1083   ∈ wcel 2113  Vcvv 3497   ⊆ wss 3939   × cxp 5556  ⟶wf 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-xp 5564  df-rel 5565  df-cnv 5566  df-dm 5568  df-rn 5569  df-fun 6360  df-fn 6361  df-f 6362

This theorem is referenced by:  elmapg  8422  f1oen2g  8529  f1dom2g  8530  dom3d  8554  domssex2  8680  domssex  8681  mapxpen  8686  oismo  9007  wdomima2g  9053  ixpiunwdom  9058  dfac8clem  9461  acni2  9475  acnlem  9477  dfac4  9551  dfac2a  9558  axdc2lem  9873  axdc4lem  9880  axcclem  9882  axdclem2  9945  addex  12390  mulex  12391  seqf1olem2  13413  seqf1o  13414  limsuple  14838  limsuplt  14839  limsupbnd1  14842  caucvgrlem  15032  prdsval  16731  prdsplusg  16734  prdsmulr  16735  prdsvsca  16736  prdsds  16740  prdshom  16743  gsumval  17890  frmdplusg  18022  odinf  18693  efgtf  18851  gsumval3lem1  19028  gsumval3lem2  19029  gsumval3  19030  staffval  19621  cnfldcj  20555  cnfldds  20558  xrsadd  20565  xrsmul  20566  xrsds  20591  ocvfval  20813  cnpfval  21845  iscnp2  21850  txcn  22237  fmval  22554  fmf  22556  tsmsval  22742  tsmsadd  22758  blfvalps  22996  nmfval  23201  tngnm  23263  tngngp2  23264  tngngpd  23265  tngngp  23266  nmoffn  23323  nmofval  23326  ishtpy  23579  tcphex  23823  adjeu  29669  ismeas  31462  hgt750lemg  31929  isismty  35083  rrnval  35109