Theorem fex2 7878

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7695	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1130	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6689	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1133	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5269	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901   × cxp 5622  ⟶wf 6488

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  elmapg  8776  f1oen2g  8905  f1dom2g  8906  dom3d  8931  domssex2  9065  domssex  9066  mapxpen  9071  oismo  9445  wdomima2g  9491  dfac8clem  9942  acni2  9956  acnlem  9958  dfac4  10032  dfac2a  10040  axdc2lem  10358  axdc4lem  10365  axcclem  10367  mpoaddex  12901  addex  12902  mpomulex  12903  mulex  12904  seqf1olem2  13965  seqf1o  13966  limsuple  15401  limsuplt  15402  limsupbnd1  15405  caucvgrlem  15596  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  gsumval  18602  frmdplusg  18779  isghm  19144  odinf  19492  staffval  20774  cnfldcj  21318  cnfldds  21321  cnfldcjOLD  21331  cnflddsOLD  21334  xrsadd  21340  xrsmul  21341  xrsds  21364  ocvfval  21621  cnpfval  23178  iscnp2  23183  fmf  23889  tsmsval  24075  blfvalps  24327  nmfval  24532  tngnm  24595  tngngp2  24596  tngngpd  24597  tngngp  24598  nmoffn  24655  nmofval  24658  ishtpy  24927  tcphex  25173  elno  27613  adjeu  31964  ismeas  34356  isismty  38002  rrnval  38028  subex  42502  absex  42503  cjex  42504  sn-isghm  42916