Theorem fvex 3808

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

Assertion

Ref	Expression
fvex	|- (F` A) e. V

Proof of Theorem fvex

Step	Hyp	Ref	Expression
1		df-fv 3253	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 1958	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 2558	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 1851	. . . . . . . 8 |- x e. V
5	4	unisn 2565	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1561	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1451	. . . . 5 |- (E*x x = U.(F"{A}) -> E*x(F"{A}) = {x})
8	2, 7	ax-mp 7	. . . 4 |- E*x(F"{A}) = {x}
9		moabex 2819	. . . 4 |- (E*x(F"{A}) = {x} -> {x | (F"{A}) = {x}} e. V)
10	8, 9	ax-mp 7	. . 3 |- {x | (F"{A}) = {x}} e. V
11	10	uniex 2924	. 2 |- U.{x | (F"{A}) = {x}} e. V
12	1, 11	eqeltri 1581	1 |- (F` A) e. V

Syntax hints:   = wceq 988   e. wcel 990  E*wmo 1414  {cab 1499  Vcvv 1849  {csn 2454  U.cuni 2551  "cima 3228  ` cfv 3237

This theorem is referenced by:  tz6.12i 3817  dffn5 3834  fvelrnb 3836  funimass4 3839  fvelimab 3841  fniinfv 3842  funfv 3846  dmfco 3849  fvco 3850  funfvop 3879  fvimacnvi 3880  fvimacnv 3881  funconstss 3884  fvimacnvALT 3885  fvelrn 3888  dff3 3893  fsn2 3912  fnressn 3913  funfvima3 3930  fvresex 3933  fniunfv 3941  funiunfv 3942  elunirnALT 3945  dff13 3950  isomin 3975  isoini 3976  f1oiso 3980  tfrlem10 3996  tfrlem11 3997  tz7.44lem1 4003  tz7.44-2 4005  rdgsucopab 4022  rdglim2a 4026  frsucopab 4030  abianfplem 4037  oprex 4059  elxp7 4179  xpopth 4183  2ndrn 4187  dfopab2 4190  dfoprab3 4191  dfoprab3s 4192  dfoprab3sOLD 4193  dfoprab4sOLD 4195  elopabi 4197  eloprabi 4198  foprab2 4199  fnoa 4232  fnom 4233  oav 4234  omv 4235  oev 4237  en1 4513  mapsnen 4516  xpdom2 4529  pw2en 4533  mapxpen 4584  xpmapenlem4 4588  xpmapenlem5 4589  phplem4 4600  unifi 4642  fiint 4644  fodomfi 4650  inf0 4692  inf3lemd 4698  inf3lem1 4699  inf3lem2 4700  inf3lem3 4701  inf3lem6 4704  trcl 4731  tz9.1 4732  r1suc 4738  r1ord 4741  rankval2 4756  rankr1 4760  bndrank 4768  rankuni2 4776  rankr1id 4783  rankuni 4784  rankr1b 4785  rankval4 4788  rankelun 4793  rankxpsuc 4801  scott0 4803  aceq3lem 4818  aceq4 4820  aceq5 4826  aceq6b 4828  numthlem 4869  unidom 4894  oncardon 4906  oncardid 4907  cardon 4914  cardid 4915  oncard 4916  unsnen 4922  sdomsdomcard 4937  cardidm 4938  ondomon 4945  cardiun 4948  cardprc 4950  alephon 4954  alephsuc 4955  alephcard 4956  alephsucpw 4959  aleph1 4960  alephordi 4963  alephsucdom 4969  cardaleph 4974  alephiso 4981  alephfplem1 4985  alephfplem2 4986  alephval3 4992  cflem 4994  cardcf 5000  cflecard 5001  cda1en 5015  recidpq 5160  recclpq 5161  recrecpq 5162  dmrecpq 5163  ltrpq 5174  1pr 5206  addclprlem1 5207  addclprlem2 5208  mulclprlem 5210  1idpr 5222  prlem936a 5242  prlem936 5244  reclem1pr 5245  reclem2pr 5246  reclem3pr 5247  reclem4pr 5248  seq1lem1 6602  seq1fnlem 6606  seq1val2 6607  seq11lem 6608  seq1suclem 6609  shftfn 6636  shftval 6639  seqzres2 6684  serzcl1i 6685  expval 6693  absval 6885  sumex 7104  sumeq2 7108  fsumserz2 7126  serzfsum 7127  serzrefi 7174  serz0 7176  serzcmp0 7178  serzmulci 7181  climconst3 7219  climsub 7253  climcmplem 7260  climcmpc1 7262  iserzcmp0 7266  caucvg3i 7290  iserzabslem 7301  iserzabsi 7302  cvgcmp3cei 7310  isumval2 7317  isumclim3 7323  isumclim4 7324  isum1p 7329  isummulc1 7335  isummulc1iALT 7336  isumcmpii 7338  isumspliti 7339  cvgratlem3ALT 7372  cvgratlem3 7375  efseq0ex 7434  efcl 7435  ef0 7458  efcji 7459  efaddlem26 7486  efaddlem28 7488  eftlexiOLD 7500  effsumlei 7521  efm1limi 7535  eflegeolem2 7538  acdc3lem 7611  acdclem 7619  acdcALT 7621  aleph1re 7676  infmap2lem1 7704  alephadd 7707  alephmul 7708  alephexp1 7709  alephsuc3 7710  alephexp2 7711  gch-kn 7712  tgcl 7748  lpval 7863  opntop 7990  lmfex 8079  metcnp4lem1 8088  xplmi 8093  xplmi2 8094  xplm 8095  xpcn 8096  oprcn 8097  bopcnlem1 8101  bopcnlem2 8102  bopcnlem4 8104  addcn 8106  subcn 8107  mulcn 8108  fsumcnlem 8109  bafval 8342  nvvop 8347  imsval 8435  imsmetlem 8442  sqcn 8454  ipfval 8471  ip1cnilem2 8493  ip1cnilem3 8494  sspval 8501  lnoval 8532  islno 8533  nmofval 8544  nmoval 8545  nmosetn0 8547  nmolb 8553  0ofval 8566  0oval 8567  0oo 8568  nmlno0lem 8572  lnon0 8577  blocni 8584  ajfval 8588  isph 8600  phpar 8602  ubthlem1 8648  ubthlem3 8650  ubthlem6 8653  minveclem31 8694  minveclem33 8696  minveceu 8702  hlex 8719  htthlem11 8749  efgh 8837  efghgrpilem 8838  efif 8840  efifo 8848  efif1 8856  shftefif1olem 8860  eff1i 8863  effoi 8864  normval 9110  projlem23 9328  projlem31 9336  hsupcl 9427  sshjval 9440  sshjval3 9446  pjspansn 9620  nmopsetn0 9910  nmfnsetn0 9923  eigvalval 9941  nmoplb 9949  nmfnlb 9966  adj1 9975  nmlnop0iALT 10037  nmcopexlem1 10068  nmcfnexlem1 10097  branmfn 10155  hstrlem2 10304  atomli 10427  neifil 10706  eloi 10794  aidm 10818  ishoma 10850  ishomb 10851  ismona 10872  isepia 10882  cinvlem1 10890  cinvlem2 10891  isfuna 10896  idfisf 10902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-uni 2552  df-fv 3253

Copyright terms: Public domain