Theorem fex2 7892

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 5229, but depends on ax-un 7691, 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 7706	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
2	1	3adant1 1130	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)
3		fssxp 6697	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
4	3	3ad2ant1 1133	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵))
5	2, 4	ssexd 5274	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911   × cxp 5629  ⟶wf 6495

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-fun 6501  df-fn 6502  df-f 6503

This theorem is referenced by:  elmapg  8789  f1oen2g  8917  f1dom2g  8918  dom3d  8942  domssex2  9078  domssex  9079  mapxpen  9084  oismo  9469  wdomima2g  9515  dfac8clem  9961  acni2  9975  acnlem  9977  dfac4  10051  dfac2a  10059  axdc2lem  10377  axdc4lem  10384  axcclem  10386  mpoaddex  12923  addex  12924  mpomulex  12925  mulex  12926  seqf1olem2  13983  seqf1o  13984  limsuple  15420  limsuplt  15421  limsupbnd1  15424  caucvgrlem  15615  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdshom  17406  gsumval  18580  frmdplusg  18757  isghm  19123  odinf  19469  staffval  20726  cnfldcj  21249  cnfldds  21252  cnfldcjOLD  21262  cnflddsOLD  21265  xrsadd  21272  xrsmul  21273  xrsds  21302  ocvfval  21551  cnpfval  23097  iscnp2  23102  fmf  23808  tsmsval  23994  blfvalps  24247  nmfval  24452  tngnm  24515  tngngp2  24516  tngngpd  24517  tngngp  24518  nmoffn  24575  nmofval  24578  ishtpy  24847  tcphex  25093  elno  27533  adjeu  31791  ismeas  34162  isismty  37768  rrnval  37794  subex  42208  absex  42209  cjex  42210  sn-isghm  42634