Theorem fex2 7888

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

Assertion

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

Proof of Theorem fex2

Step	Hyp	Ref	Expression
1		xpexg 7705	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1131	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6697	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1134	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5271	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903   × cxp 5630  ⟶wf 6496

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  elmapg  8788  f1oen2g  8917  f1dom2g  8918  dom3d  8943  domssex2  9077  domssex  9078  mapxpen  9083  oismo  9457  wdomima2g  9503  dfac8clem  9954  acni2  9968  acnlem  9970  dfac4  10044  dfac2a  10052  axdc2lem  10370  axdc4lem  10377  axcclem  10379  mpoaddex  12913  addex  12914  mpomulex  12915  mulex  12916  seqf1olem2  13977  seqf1o  13978  limsuple  15413  limsuplt  15414  limsupbnd1  15417  caucvgrlem  15608  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  gsumval  18614  frmdplusg  18791  isghm  19156  odinf  19504  staffval  20786  cnfldcj  21330  cnfldds  21333  cnfldcjOLD  21343  cnflddsOLD  21346  xrsadd  21352  xrsmul  21353  xrsds  21376  ocvfval  21633  cnpfval  23190  iscnp2  23195  fmf  23901  tsmsval  24087  blfvalps  24339  nmfval  24544  tngnm  24607  tngngp2  24608  tngngpd  24609  tngngp  24610  nmoffn  24667  nmofval  24670  ishtpy  24939  tcphex  25185  elno  27625  adjeu  31977  ismeas  34377  isismty  38052  rrnval  38078  subex  42617  absex  42618  cjex  42619  sn-isghm  43031