MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnex Structured version   Visualization version   GIF version

Theorem fnex 7237
Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 7235. See fnexALT 7975 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fnex ((𝐹 Fn 𝐴𝐴𝐵) → 𝐹 ∈ V)

Proof of Theorem fnex
StepHypRef Expression
1 fnrel 6670 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 df-fn 6564 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3 eleq1a 2836 . . . . . 6 (𝐴𝐵 → (dom 𝐹 = 𝐴 → dom 𝐹𝐵))
43impcom 407 . . . . 5 ((dom 𝐹 = 𝐴𝐴𝐵) → dom 𝐹𝐵)
5 resfunexg 7235 . . . . 5 ((Fun 𝐹 ∧ dom 𝐹𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
64, 5sylan2 593 . . . 4 ((Fun 𝐹 ∧ (dom 𝐹 = 𝐴𝐴𝐵)) → (𝐹 ↾ dom 𝐹) ∈ V)
76anassrs 467 . . 3 (((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ∧ 𝐴𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
82, 7sylanb 581 . 2 ((𝐹 Fn 𝐴𝐴𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
9 resdm 6044 . . . 4 (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
109eleq1d 2826 . . 3 (Rel 𝐹 → ((𝐹 ↾ dom 𝐹) ∈ V ↔ 𝐹 ∈ V))
1110biimpa 476 . 2 ((Rel 𝐹 ∧ (𝐹 ↾ dom 𝐹) ∈ V) → 𝐹 ∈ V)
121, 8, 11syl2an2r 685 1 ((𝐹 Fn 𝐴𝐴𝐵) → 𝐹 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  Vcvv 3480  dom cdm 5685  cres 5687  Rel wrel 5690  Fun wfun 6555   Fn wfn 6556
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-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569
This theorem is referenced by:  fnexd  7238  funex  7239  fex  7246  offval  7706  fndmexb  7928  suppvalfn  8193  suppfnss  8214  fnsuppeq0  8217  wfrlem15OLD  8363  fndmeng  9075  fdmfifsupp  9415  cfsmolem  10310  axcc2lem  10476  unirnfdomd  10607  prdsbas2  17514  prdsplusgval  17518  prdsmulrval  17520  prdsleval  17522  prdsdsval  17523  prdsvscaval  17524  xpscf  17610  brssc  17858  sscpwex  17859  ssclem  17863  isssc  17864  rescval2  17872  reschom  17874  rescabsOLD  17878  isfuncd  17910  dprdw  20030  prdsmgp  20148  dsmmbas2  21757  dsmmelbas  21759  ptval  23578  prdstopn  23636  qtoptop  23708  imastopn  23728  fnpreimac  32681  suppss3  32735  ofcfval  34099  dya2iocuni  34285  tfsconcatun  43350  stoweidlem27  46042  stoweidlem59  46074  omeiunle  46532  preimafvelsetpreimafv  47375  fundcmpsurinjlem2  47386
  Copyright terms: Public domain W3C validator