Theorem fvex 4778

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 4147	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 2676	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 3375	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 2541	. . . . . . . 8 |- x e. _V
5	4	unisn 3382	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 2194	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 2079	. . . . 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 3676	. . . 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 3933	. 2 |- U.{x | (F"{A}) = {x}} e. _V
12	1, 11	eqeltri 2214	1 |- (F` A) e. _V

Syntax hints:   = wceq 1586   e. wcel 1588  E*wmo 2038  {cab 2128  _Vcvv 2538  {csn 3238  U.cuni 3366  "cima 4122  ` cfv 4131

This theorem is referenced by:  tz6.12i 4787  dffn5 4803  fvelrnb 4805  funimass4 4808  fvelimab 4810  fniinfv 4811  funfv 4816  dmfco 4821  fvco 4822  funfvop 4862  fvimacnvi 4863  fvimacnv 4864  funconstss 4867  fvimacnvALT 4868  fvelrn 4875  dff3 4880  fsn2 4903  fnressn 4905  funfvima3 4922  fvresex 4926  fniunfv 4936  funiunfv 4937  elunirnALT 4941  dff13 4945  isomin 4972  isoini 4973  f1oiso 4977  oprex 5003  elxp7 5150  xpopth 5157  2ndrn 5161  dfopab2 5164  dfoprab3 5165  dfoprab3s 5166  oprabopabf 5170  elopabi 5172  eloprabi 5173  foprab2 5174  oprabco 5187  iunfoprab 5195  fparlem1 5204  fparlem2 5205  fpar 5208  fnwelem 5215  smoiso 5273  smoiso2 5280  tfrlem10 5292  tfrlem11 5293  tz7.44lem1 5299  tz7.44-2 5301  rdgsucopab 5318  rdglim2a 5322  frsucopab 5326  abianfplem 5337  fnoa 5359  fnom 5360  oav 5361  omv 5362  oev 5364  en1 5646  mapsnen 5650  mapsnenOLD 5651  xpdom2 5665  pw2en 5671  ac6sfilem3 5674  ac6sfi 5675  riotaex 5733  mapxpen 5780  xpmapenlem4 5784  xpmapenlem5 5785  phplem4 5797  unifi 5870  fiint 5872  fodomfi 5880  ordiso 5914  inf0 5944  inf3lemd 5950  inf3lem1 5951  inf3lem2 5952  inf3lem3 5953  inf3lem6 5956  trcl 5988  tz9.1 5989  r1suc 5999  r1ord 6002  rankval2 6017  rankr1 6021  bndrank 6029  rankuni2 6037  rankr1id 6044  rankuni 6045  rankr1b 6046  rankval4 6049  rankelun 6054  rankxpsuc 6062  scott0 6086  cardid2 6108  oncardonOLD 6110  oncardid 6111  oncard 6115  cardiun 6137  cardmin2 6138  leweon 6145  r0weon 6146  infxpenlem 6147  infxpidm2 6149  alephon 6154  alephordi 6159  omsubsuc 6168  omsubsuc2 6169  omsubsdomlem2 6171  omsubsdom 6172  omsubdom 6173  omsubel 6174  elomsubsd 6176  omsublim 6178  infenomsub 6180  aceq3lem 6186  aceq4 6188  aceq5 6194  aceq6b 6196  aceq8alem 6198  alephnbtwn2 6210  alephiso 6221  alephfplem1 6227  alephfplem2 6228  alephval3 6233  alephsucpw2 6234  nnaun 6262  pwsdompw 6264  cflem 6265  cardcf 6271  cflecard 6272  cff1 6278  cfflb 6279  cfval2 6280  cflim3 6282  cflim2 6283  cfsmolem 6285  axcc2lem 6293  domtriomlem 6296  domtriomlemOLD 6298  dcomex 6302  axdc2lem 6303  axdc3lem2 6306  axdc3lem4 6308  axcclem 6312  numthlem 6355  axdclem 6371  axdclem2 6372  unidom 6384  cardonOLD 6390  cardid 6391  oncardOLD 6392  unsnen 6399  sdomsdomcard 6413  cardidmOLD 6414  infxpidm 6416  ondomon 6422  cardprcOLD 6426  alephsucOLD 6428  konigthlem 6429  alephcardOLD 6431  alephsucpw 6434  aleph1 6435  alephordiOLD 6438  alephsucdomOLD 6441  cardalephOLD 6443  alephreg 6449  pwcfsdom 6450  cfpwsdom 6451  cda1enOLD 6453  nnaunOLD 6456  recidpq 6589  recclpq 6590  recrecpq 6591  dmrecpq 6592  ltrpq 6603  1pr 6635  addclprlem1 6636  addclprlem2 6637  mulclprlem 6639  1idpr 6651  prlem936a 6671  prlem936 6673  reclem1pr 6674  reclem2pr 6675  reclem3pr 6676  reclem4pr 6677  fzennn 8090  cardfz 8091  cardfzOLD 8092  seq1lem1 8095  seq1fnlem 8099  seq1val2 8100  seq11lem 8101  seq1suclem 8102  shftfn 8131  shftval 8134  seqzres2 8183  serzcl1i 8189  expval 8197  absval 8396  fz1fi 8614  sumex 8637  sumeq2 8641  fsumserz2 8659  serzfsum 8660  serzrefi 8707  serz0 8709  serzcmp0 8711  serzmulci 8714  climconst3 8752  climsub 8786  climcmplem 8793  climcmpc1 8795  iserzcmp0 8799  caucvg3i 8823  iserzabslem 8834  iserzabsi 8835  cvgcmp3cei 8844  isumval2 8851  isumclim3 8857  isumclim4 8858  isum1p 8863  isummulc1 8869  isummulc1iALT 8870  isumcmpii 8872  isumspliti 8873  supcvglem 8876  explecnv 8893  cvgratlem3ALT 8909  cvgratlem3 8912  efseq0ex 8971  efcl 8972  ef0 8995  efcji 8996  efaddlem26 9023  efaddlem28 9025  eftlexiOLD 9037  eftlex 9038  effsumlei 9060  efm1limi 9074  eflegeolem2 9077  acdc3lem 9152  acdclem 9161  acdcALT 9163  aleph1re 9214  infmap2lem1 9242  alephadd 9245  alephmul 9246  alephexp1 9247  alephsuc3 9248  alephexp2 9249  gch-kn 9250  mulgcdlem2 9352  1arithlem12 9405  1arithlem13 9406  1arithlem22 9415  strcval 9428  str2v1 9435  str2v2 9436  isgrp 9464  grpstr 9468  grpinvfval 9490  isring 9508  divrngmcl 9529  divrngidlem 9530  divrngid 9531  invrfval 9535  invrcl 9536  ispos 9548  isposix 9554  pltval 9556  lubfval 9572  lubval 9573  lubprop 9574  glbfval 9577  glbval 9578  glbprop 9579  joinfval 9581  joinval 9582  joinlem 9584  meetfval 9588  meetval 9589  meetlem 9591  p0val 9604  p1val 9605  clatlem 9672  tpsstr 9730  tgcl 9745  indistps2 9778  indistps2ALT 9780  txval 9790  lpval 9885  cnpnei 9909  opntop 10013  lmfex 10103  metcnp4lem1 10112  xplmi 10117  xplmi2 10118  xplm 10119  xpcn 10120  oprcn 10121  bopcnlem1 10125  bopcnlem2 10126  bopcnlem4 10128  addcn 10130  subcn 10131  mulcn 10132  fsumcnlem 10133  grp2grpo 10190  gxval 10250  gaid 10323  bafval 10424  nvvop 10429  imsval 10517  imsmetlem 10524  vacnlem4 10539  vacnlem5 10540  vacnlem6 10541  sqcn 10543  ipfval 10560  ip1cnilem2 10582  ip1cnilem3 10583  sspval 10590  lnoval 10621  islno 10622  nmofval 10633  nmoval 10634  nmosetn0 10636  nmolb 10642  0ofval 10656  0oval 10657  0oo 10658  nmlno0lem 10662  lnon0 10667  blocni 10674  ajfval 10678  isph 10691  phpar 10693  ajval 10732  ubthlem1 10741  ubthlem3 10743  ubthlem6 10746  minveclem31 10790  minveclem33 10792  minveceu 10799  hlex 10818  htthlem11 10848  efgh 10943  efghgrpilem 10944  efif 10946  efifo 10954  efif1 10962  shftefif1olem 10966  eff1i 10969  effoi 10970  upxp 11060  uptx 11061  txcnopab 11063  stoig2 11090  stoig3 11091  fbssint 11117  fsubbas 11119  fgfil 11128  neifil 11140  hausfillim 11141  isfilmap 11146  sflimf 11156  unmnd 11243  dvrunz 11257  normval 11460  projlem23 11675  projlem31 11683  hsupcl 11774  sshjval 11787  sshjval3 11793  pjspansn 11967  nmopsetn0 12261  nmfnsetn0 12274  eigvalval 12292  nmoplb 12300  nmfnlb 12317  adj1 12326  nmlnop0iALT 12389  nmcopexlem1 12420  nmcfnexlem1 12449  branmfn 12507  hstrlem2 12662  atomli 12785  bnj134 13258  bnj522 14032  bnj535 14036  bnj546 14043  bnj889 14094  bnj1421 14303  bnj1442 14311  trpredtr 14582  trpredmintr 14583  trpredrec 14590  wfrlem13 14622  wfrlem14 14623  sltval2 14662  sltsgn1 14667  sltsgn2 14668  sltintdifex 14669  sltres 14670  axdenselem8 14695  axdense 14696  nocvxmin 14698  axfelem9 14707  axfelem10 14708  prj1b 15105  prj3 15106  eloi 15112  inpreima5 15180  prmapcp3 15237  valpr 15238  repfuntw 15241  cbicplem 15247  valcurfn 15290  defse3 15353  prodex 15395  fincmpzer 15446  seqzp2 15451  expmiz 15459  expm 15460  fnopabco2b 15469  curgrpact 15470  fprodneg 15476  rngunval2 15527  mulveczer 15575  mulinvsca 15576  muldisc 15577  svli2 15579  svs2 15582  bintop 15658  intopcoaconb 15662  intopcoaconc 15663  subtopsin2 15669  usptoplem 15682  istopx 15683  prtoptop 15684  prcnt 15686  limvinlv 15707  iscnp3 15712  trhom 15761  grphmlem1 15769  grphlem3 15771  grphm 15774  stoi 15789  cntrsetlem 15791  aidm2 15891  dmrngcmp 15892  dualalg 15925  dualded 15926  dualcat2 15927  ishoma 15930  ishomb 15931  ismona 15952  isepia 15962  cinvlem1 15970  cinvlem2 15971  isfuna 15976  idfisf 15983  issubcat 15987  idsubfun 16000  infemb 16001  tarax3d4 16037  vtarsu 16073  tartarmap 16075  trclval 16081  fictblem 16194  fictb 16195  ordisoOLD 16198  hartoglem 16207  omsubsucOLD 16210  omsubsuc2OLD 16211  omsubsdomlem2OLD 16213  omsubsdomOLD 16214  omsubdomOLD 16215  omsubelOLD 16216  elomsubsdOLD 16218  omsublimOLD 16220  infenomsubOLD 16222  subntr 16249  compsub 16255  hscptsscld 16258  compfipin0lem 16259  alexsublem2 16262  alexsublem4 16264  alexsub 16265  2ndc1stc 16301  neibastop2lem1 16343  neibastop2lem3 16345  neibastop2lem4 16346  flimcls 16412  filclus 16429  fclsfnflim 16438  fcluscomplem 16444  fcluscomp 16445  sfclusf 16448  tailmap 16460  tailuni 16462  tailfb 16463  filnetlem5 16468  filnet 16469  fnopabco 16535  upixp 16553  ac6gf 16573  indexdom 16578  sdclem1 16633  sdclem2 16634  sdc 16635  fdc 16636  fdc1 16637  fsumltisumii 16646  fsumltisumi 16647  fsumleisumii 16649  neificl 16665  mettrifi 16671  geomcau 16673  heiborlem1 16779  heiborlem2 16780  heiborlem4 16782  heiborlem8 16786  heiborlem23 16801  heiborlem33 16811  bfplem3 16824  bfplem8 16829  rrnmval 16838  rrndm 16839  rrnmet 16840  rrncms 16843  rrntotbndlem2 16845  grpkerinj 16866  phtpyid 16873  phtpycolem3 16877  phtpycolem4 16878  reparphtlem1 16887  reparphtlem2 16888  pcoval1 16898  pcoval2 16899  pcocn 16900  pcopt 16908  pcoass 16909  pcorev 16911  elpi1 16913  pi1f 16917  pi1val 16918  pi1gp 16919  isringd 16921  isdivrng1 16933  isdivrng2 16935  rnghomval 16942  isrnghom 16943  iscring2 16970  idlval 16985  isidl 16986  0idl 16997  0ring 16999  divrngidl 17000  intidl 17001  keridl 17004  pridlval 17005  maxidlval 17011  smprngpr 17024  igenval 17033  fveqsb 17255  smoisoOLD 17275  addrcom 17297  isopos 17576  cmtfval 17604  cvrfval 17660  pats 17676  glbcon 17770  glbconx 17771  issrng 17888  islvec 17900  isphil 17907  plusssfval 17916  plusssval 17917  ocvfval 17918  ocvval 17919  csubspset 17920  iscsubsp 17921  llnset 17937  lplnset 17960  lvolset 18004  lineset 18171  isline 18172  pointset 18174  psubspset 18177  ispsubsp 18178  pmapfval 18188  pmapval 18189  paddfval 18229  paddval 18230  polfval 18321  polval 18322  psubclset 18350  ispsubcl 18351  watfval 18405  watval 18406  lhpset 18408  lautset 18437  islaut 18438  pautset 18452  ispaut 18453  ldilfset 18462  ldilset 18463  ltrnfset 18470  ltrnset 18471  dilfset 18497  dilset 18498  trnfset 18500  trnset 18501  trlfset 18505  trlset 18506  cdleme25cl 18729  cdleme26e 18731  cdleme26eALT 18733  cdleme26fALT 18734  cdleme26f 18735  cdleme26f2ALT 18736  cdleme26f2 18737  cdleme29cl 18750  cdlemefrs29cl 18773  cdlemefs32sn1aw 18788  cdleme43fsv1snlem 18794  cdleme41sn3a 18808  cdleme32a 18817  cdleme40m 18843  cdleme40nOLD 18844  cdleme40n 18845  cdleme42b 18857

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-uni 3367  df-fv 4147

Copyright terms: Public domain