Theorem fex2 7930

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

Assertion

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

Proof of Theorem fex2

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926   × cxp 5652  ⟶wf 6526

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-dm 5664  df-rn 5665  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  elmapg  8851  f1oen2g  8981  f1dom2g  8982  dom3d  9006  domssex2  9149  domssex  9150  mapxpen  9155  oismo  9552  wdomima2g  9598  dfac8clem  10044  acni2  10058  acnlem  10060  dfac4  10134  dfac2a  10142  axdc2lem  10460  axdc4lem  10467  axcclem  10469  mpoaddex  13002  addex  13003  mpomulex  13004  mulex  13005  seqf1olem2  14058  seqf1o  14059  limsuple  15492  limsuplt  15493  limsupbnd1  15496  caucvgrlem  15687  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  gsumval  18653  frmdplusg  18830  isghm  19196  odinf  19542  staffval  20799  cnfldcj  21322  cnfldds  21325  cnfldcjOLD  21335  cnflddsOLD  21338  xrsadd  21345  xrsmul  21346  xrsds  21375  ocvfval  21624  cnpfval  23170  iscnp2  23175  fmf  23881  tsmsval  24067  blfvalps  24320  nmfval  24525  tngnm  24588  tngngp2  24589  tngngpd  24590  tngngp  24591  nmoffn  24648  nmofval  24651  ishtpy  24920  tcphex  25167  elno  27607  adjeu  31816  ismeas  34176  isismty  37771  rrnval  37797  subex  42245  absex  42246  cjex  42247  sn-isghm  42643