Theorem fex2 7982

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7796	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1148	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6767	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1151	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5293	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   × cxp 5656  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-dm 5668  df-rn 5669  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  elmapg  8897  f1oen2g  9033  f1dom2g  9034  dom3d  9059  domssex2  9194  domssex  9195  mapxpen  9200  oismo  9571  wdomima2g  9617  dfac8clem  10150  acni2  10164  acnlem  10166  dfac4  10240  dfac2a  10247  axdc2lem  10565  axdc4lem  10572  axcclem  10574  mpoaddex  13156  addex  13157  mpomulex  13158  mulex  13159  seqf1olem2  14225  seqf1o  14226  absex  15549  limsuple  15689  limsuplt  15690  limsupbnd1  15693  caucvgrlem  15884  prdsplusg  17679  prdsmulr  17680  prdsvsca  17681  prdshom  17688  gsumval  18916  frmdplusg  19100  isghm  19480  odinf  19828  staffval  21149  cnfldcj  21738  cnfldds  21741  xrsadd  21748  xrsmul  21749  xrsds  21768  ocvfval  22027  cnpfval  23607  iscnp2  23612  fmf  24319  tsmsval  24505  blfvalps  24757  nmfval  24962  tngnm  25025  tngngp2  25026  tngngpd  25027  tngngp  25028  nmoffn  25085  nmofval  25088  ishtpy  25348  tcphex  25593  elno  28060  adjeu  32548  ismeas  34943  isismty  39001  rrnval  39027  subex  43565  cjex  43566  sn-isghm  43950  grpgimcanon  46192