Theorem fnex 7216

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 7214. See fnexALT 7948 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

Step	Hyp	Ref	Expression
1		fnrel 6634	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		df-fn 6536	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3		eleq1a 2855	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → (dom 𝐹 = 𝐴 → dom 𝐹 ∈ 𝐵))
4	3	impcom 413	. . . . 5 ⊢ ((dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵) → dom 𝐹 ∈ 𝐵)
5		resfunexg 7214	. . . . 5 ⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
6	4, 5	sylan2 605	. . . 4 ⊢ ((Fun 𝐹 ∧ (dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵)) → (𝐹 ↾ dom 𝐹) ∈ V)
7	6	anassrs 473	. . 3 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ∧ 𝐴 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
8	2, 7	sylanb 593	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V)
9		resdm 6019	. . . 4 ⊢ (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
10	9	eleq1d 2845	. . 3 ⊢ (Rel 𝐹 → ((𝐹 ↾ dom 𝐹) ∈ V ↔ 𝐹 ∈ V))
11	10	biimpa 482	. 2 ⊢ ((Rel 𝐹 ∧ (𝐹 ↾ dom 𝐹) ∈ V) → 𝐹 ∈ V)
12	1, 8, 11	syl2an2r 698	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450  dom cdm 5655   ↾ cres 5657  Rel wrel 5660  Fun wfun 6527   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541

This theorem is used by:  fnexd  7217  funex  7218  fex  7225  offval  7687  fndmexb  7903  suppvalfn  8166  suppfnss  8187  fnsuppeq0  8190  fndmeng  9042  fdmfifsupp  9345  cfsmolem  10272  axcc2lem  10438  unirnfdomd  10576  prdsbas2  17554  prdsplusgval  17558  prdsmulrval  17560  prdsleval  17562  prdsdsval  17563  prdsvscaval  17564  xpscf  17651  brssc  17903  sscpwex  17904  ssclem  17908  isssc  17909  rescval2  17917  reschom  17919  isfuncd  17954  dprdw  20139  prdsmgp  20284  dsmmbas2  21950  dsmmelbas  21952  ptval  23796  prdstopn  23854  qtoptop  23926  imastopn  23946  fnpreimac  33143  suppss3  33194  ofcfval  34608  dya2iocuni  34794  tfsconcatun  44178  stoweidlem27  46855  stoweidlem59  46887  omeiunle  47345  preimafvelsetpreimafv  48288  fundcmpsurinjlem2  48299