Theorem fvex 2838

Description: The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.

Assertion

Ref	Expression
fvex	⊢ (F ‘A) ∈ V

Proof of Theorem fvex

Step	Hyp	Ref	Expression
1		df-fv 2438	. 2 ⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}
2		unieq 1927	. . . . . . 7 ⊢ ((F “ {A}) = {x} → ∪(F “ {A}) = ∪{x})
3		visset 1350	. . . . . . . 8 ⊢ x ∈ V
4	3	unisn 1932	. . . . . . 7 ⊢ ∪{x} = x
5	2, 4	syl6req 1141	. . . . . 6 ⊢ ((F “ {A}) = {x} → x = ∪(F “ {A}))
6	5	ax-gen 677	. . . . 5 ⊢ ∀x((F “ {A}) = {x} → x = ∪(F “ {A}))
7		moeq 1431	. . . . 5 ⊢ ∃*x x = ∪(F “ {A})
8		immo 1043	. . . . 5 ⊢ (∀x((F “ {A}) = {x} → x = ∪(F “ {A})) → (∃*x x = ∪(F “ {A}) → ∃*x(F “ {A}) = {x}))
9	6, 7, 8	mp2 43	. . . 4 ⊢ ∃*x(F “ {A}) = {x}
10		moabex 1868	. . . 4 ⊢ (∃*x(F “ {A}) = {x} → {x∣(F “ {A}) = {x}} ∈ V)
11	9, 10	ax-mp 6	. . 3 ⊢ {x∣(F “ {A}) = {x}} ∈ V
12	11	uniex 1947	. 2 ⊢ ∪{x∣(F “ {A}) = {x}} ∈ V
13	1, 12	eqeltr 1159	1 ⊢ (F ‘A) ∈ V

Syntax hints:   → wi 2  ∀wal 672  ∃*wmo 1008  {cab 1090   = wceq 1091   ∈ wcel 1092  Vcvv 1348  {csn 1808  ∪cuni 1919   “ cima 2413   ‘cfv 2422

This theorem is referenced by:  tz6.12i 2847  fnopabfv 2858  fniunfv 2860  funfv 2862  dmfco 2864  fvco 2865  fvelrn 2883  funopfv 2886  fvrn 2888  fsn2 2896  fnressn 2897  funfvima3 2906  fvresex 2909  f1fv 2916  isomin 2937  isoini 2938  f1oiso 2942  tfrlem10 2958  tfrlem11 2959  tz7.44lem1 2965  tz7.44-2 2967  rdgsucopab 2984  rdglim2a 2988  frsucopab 2992  abianfplem 2999  oprex 3018  fnoa 3117  fnom 3118  oav 3119  omv 3120  oev 3122  en1 3331  mapsnen 3334  xpdom2 3345  pw2en 3348  mapxpen 3390  xpmapenlem4 3394  xpmapenlem5 3395  phplem5 3407  fiint 3445  inf0 3457  inf3lemd 3463  inf3lem1 3464  inf3lem2 3465  inf3lem3 3466  inf3lem6 3469  trcl 3489  tz9.1 3490  r1suc 3496  r1ord 3499  rankval2 3514  rankr1 3518  bndrank 3526  rankuni 3533  rankr1id 3539  ranklon 3540  scott0 3542  aceq3lem 3555  aceq4 3557  aceq5 3563  aceq6b 3565  numthlem 3598  oncardon 3627  oncardid 3628  cardon 3634  cardid 3635  oncard 3636  sdomsdomcard 3654  cardcard 3655  ondomon 3662  cardiun 3665  cardprc 3667  alephon 3671  alephsuc 3672  alephcard 3673  aleph1 3676  alephordi 3679  alephsucdom 3685  cardaleph 3690  alephiso 3697  cflem 3700  cardcf 3706  cflecard 3707  cda1en 3721  recidpq 3865  recclpq 3866  recrecpq 3867  dmrecpq 3868  ltrpq 3879  1pr 3911  addclprlem1 3912  addclprlem2 3913  mulclprlem 3915  1idpr 3927  prlem936a 3947  prlem936 3949  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  reclem4pr 3953  seqlem1 4662  seqfnlem 4666  seqval2 4667  seq1lem 4668  seqsuclem 4669  expvalt 4677  absvalt 4801  infmap2lem1 4951  alephexp1 4954  alephsuc3 4955  alephexp2 4956  gch-kn 4957  normvalt 5075  projlem23 5215  projlem25 5217  projlem31 5223  hsupclt 5308  sshjvalt 5321  sshjval3t 5327

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-uni 1920  df-fv 2438

metamath.org