Theorem fex2 7869

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903   × cxp 5617  ⟶wf 6478

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-fun 6484  df-fn 6485  df-f 6486

This theorem is referenced by:  elmapg  8766  f1oen2g  8894  f1dom2g  8895  dom3d  8919  domssex2  9054  domssex  9055  mapxpen  9060  oismo  9432  wdomima2g  9478  dfac8clem  9926  acni2  9940  acnlem  9942  dfac4  10016  dfac2a  10024  axdc2lem  10342  axdc4lem  10349  axcclem  10351  mpoaddex  12889  addex  12890  mpomulex  12891  mulex  12892  seqf1olem2  13949  seqf1o  13950  limsuple  15385  limsuplt  15386  limsupbnd1  15389  caucvgrlem  15580  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  gsumval  18551  frmdplusg  18728  isghm  19094  odinf  19442  staffval  20726  cnfldcj  21270  cnfldds  21273  cnfldcjOLD  21283  cnflddsOLD  21286  xrsadd  21292  xrsmul  21293  xrsds  21316  ocvfval  21573  cnpfval  23119  iscnp2  23124  fmf  23830  tsmsval  24016  blfvalps  24269  nmfval  24474  tngnm  24537  tngngp2  24538  tngngpd  24539  tngngp  24540  nmoffn  24597  nmofval  24600  ishtpy  24869  tcphex  25115  elno  27555  adjeu  31833  ismeas  34166  isismty  37781  rrnval  37807  subex  42220  absex  42221  cjex  42222  sn-isghm  42646