Theorem fvex 4689

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 4014	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 2431	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 3185	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 2295	. . . . . . . 8 |- x e. _V
5	4	unisn 3193	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1945	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1814	. . . . 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 3513	. . . 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 3794	. 2 |- U.{x | (F"{A}) = {x}} e. _V
12	1, 11	eqeltri 1967	1 |- (F` A) e. _V

Syntax hints:   = wceq 1298   e. wcel 1300  E*wmo 1772  {cab 1871  _Vcvv 2292  {csn 3044  U.cuni 3177  "cima 3989  ` cfv 3998

This theorem is referenced by:  tz6.12i 4698  dffn5 4717  fvelrnb 4719  funimass4 4722  fvelimab 4725  fvelimabOLD 4726  fniinfv 4727  funfv 4731  dmfco 4735  fvco 4736  funfvop 4776  fvimacnvi 4777  fvimacnv 4778  funconstss 4781  fvimacnvALT 4782  fvelrn 4785  dff3 4790  fsn2 4809  fnressn 4812  funfvima3 4830  fvresex 4833  fniunfv 4841  funiunfv 4842  elunirnALT 4845  dff13 4850  isomin 4876  isoini 4877  f1oiso 4881  oprex 4907  elxp7 5042  xpopth 5046  2ndrn 5050  dfopab2 5053  dfoprab3 5054  dfoprab3s 5055  elopabi 5059  eloprabi 5060  foprab2 5061  iunfoprab 5072  fparlem1 5081  fparlem2 5082  fpar 5085  tfrlem10 5128  tfrlem11 5129  tz7.44lem1 5135  tz7.44-2 5137  rdgsucopab 5154  rdglim2a 5158  frsucopab 5162  abianfplem 5170  fnoa 5193  fnom 5194  oav 5195  omv 5196  oev 5198  en1 5485  mapsnen 5488  xpdom2 5501  pw2en 5505  ac6sfilem3 5508  ac6sfi 5509  riotaex 5564  mapxpen 5589  xpmapenlem4 5593  xpmapenlem5 5594  phplem4 5605  unifi 5648  fiint 5650  fodomfi 5656  ordiso 5683  hartoglem 5692  inf0 5712  inf3lemd 5718  inf3lem1 5719  inf3lem2 5720  inf3lem3 5721  inf3lem6 5724  trcl 5752  tz9.1 5753  r1suc 5763  r1ord 5766  rankval2 5781  rankr1 5785  bndrank 5793  rankuni2 5801  rankr1id 5808  rankuni 5809  rankr1b 5810  rankval4 5813  rankelun 5818  rankxpsuc 5826  scott0 5847  oncardon 5866  oncardid 5867  alephon 5876  omsubsuc 5877  omsubsuc2 5878  omsubsdomlem2 5880  omsubsdom 5881  omsubdom 5882  omsubel 5883  elomsubsd 5885  omsublim 5887  infenomsub 5889  aceq3lem 5894  aceq4 5896  aceq5 5902  aceq6b 5904  numthlem 5945  unidom 5970  cardon 5976  cardid 5977  oncard 5978  unsnen 5985  sdomsdomcard 6000  cardidm 6001  ondomon 6008  cardiun 6011  cardprc 6013  alephsuc 6014  alephcard 6015  alephsucpw 6018  aleph1 6019  alephordi 6022  alephsucdom 6028  cardaleph 6033  alephiso 6040  alephfplem1 6044  alephfplem2 6045  alephval3 6051  cflem 6053  cardcf 6059  cflecard 6060  cda1en 6076  nnaun 6089  recidpq 6223  recclpq 6224  recrecpq 6225  dmrecpq 6226  ltrpq 6237  1pr 6269  addclprlem1 6270  addclprlem2 6271  mulclprlem 6273  1idpr 6285  prlem936a 6305  prlem936 6307  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  reclem4pr 6311  cardfz 7719  seq1lem1 7722  seq1fnlem 7726  seq1val2 7727  seq11lem 7728  seq1suclem 7729  shftfn 7756  shftval 7759  seqzres2 7804  serzcl1i 7805  expval 7813  absval 8012  sumex 8241  sumeq2 8245  fsumserz2 8263  serzfsum 8264  serzrefi 8311  serz0 8313  serzcmp0 8315  serzmulci 8318  climconst3 8356  climsub 8390  climcmplem 8397  climcmpc1 8399  iserzcmp0 8403  caucvg3i 8427  iserzabslem 8438  iserzabsi 8439  cvgcmp3cei 8448  isumval2 8455  isumclim3 8461  isumclim4 8462  isum1p 8467  isummulc1 8473  isummulc1iALT 8474  isumcmpii 8476  isumspliti 8477  explecnv 8495  cvgratlem3ALT 8511  cvgratlem3 8514  efseq0ex 8573  efcl 8574  ef0 8597  efcji 8598  efaddlem26 8625  efaddlem28 8627  eftlexiOLD 8639  effsumlei 8662  efm1limi 8676  eflegeolem2 8679  acdc3lem 8754  acdclem 8763  acdcALT 8765  aleph1re 8820  infmap2lem1 8848  alephadd 8851  alephmul 8852  alephexp1 8853  alephsuc3 8854  alephexp2 8855  gch-kn 8856  tgcl 8894  txval 8932  lpval 9019  cnpnei 9043  opntop 9147  lmfex 9237  metcnp4lem1 9246  xplmi 9251  xplmi2 9252  xplm 9253  xpcn 9254  oprcn 9255  bopcnlem1 9259  bopcnlem2 9260  bopcnlem4 9262  addcn 9264  subcn 9265  mulcn 9266  fsumcnlem 9267  gxval 9381  gaid 9454  bafval 9555  nvvop 9560  imsval 9648  imsmetlem 9655  vacnlem4 9670  vacnlem5 9671  vacnlem6 9672  sqcn 9674  ipfval 9691  ip1cnilem2 9713  ip1cnilem3 9714  sspval 9721  lnoval 9752  islno 9753  nmofval 9764  nmoval 9765  nmosetn0 9767  nmolb 9773  0ofval 9787  0oval 9788  0oo 9789  nmlno0lem 9793  lnon0 9798  blocni 9805  ajfval 9809  isph 9822  phpar 9824  ajval 9863  ubthlem1 9872  ubthlem3 9874  ubthlem6 9877  minveclem31 9920  minveclem33 9922  minveceu 9928  hlex 9947  htthlem11 9977  efgh 10072  efghgrpilem 10073  efif 10075  efifo 10083  efif1 10091  shftefif1olem 10095  eff1i 10098  effoi 10099  oprabopabf 10157  oprabco 10159  dif1enOLD 10173  upxp 10225  uptx 10226  txcnopab 10228  fbssint 10279  fsubbas 10281  fgfil 10290  neifil 10302  hausfillim 10303  isfilmap 10308  sflimf 10318  unmnd 10405  dvrunz 10419  normval 10623  projlem23 10841  projlem31 10849  hsupcl 10940  sshjval 10953  sshjval3 10959  pjspansn 11133  nmopsetn0 11429  nmfnsetn0 11442  eigvalval 11460  nmoplb 11468  nmfnlb 11485  adj1 11494  nmlnop0iALT 11557  nmcopexlem1 11588  nmcfnexlem1 11617  branmfn 11675  branmfnOLD 11676  hstrlem2 11831  atomli 11954  bnj134 12478  bnj522 13261  bnj535 13265  bnj546 13272  bnj889 13323  bnj1421 13532  bnj1442 13540  mulgcdlem2 13757  trcltr 13936  wfrlem13 13969  wfrlem14 13970  sltval2 13997  sltsgn1 14002  sltsgn2 14003  sltintdifex 14004  axdenselem8 14026  axdense 14027  nocvxmin 14029  axfelem8 14038  axfelem9 14039  axfelem12 14042  prj1 14395  eloi 14400  inpreima2 14468  inpreima5 14469  prmapcp3 14498  valpr 14499  repfuntw 14502  cbicplem 14508  valcurfn 14551  defse3 14614  prodex 14656  fincmpzer 14711  seqzp2 14716  expmiz 14724  expm 14725  fnopabco2b 14734  curgrpact 14735  fprodneg 14741  rngunval2 14774  mulveczer 14822  mulinvsca 14823  muldisc 14824  svli2 14826  svs2 14829  bintop 14901  usptoplem 14917  istopx 14918  prtoptop 14919  limvinlv 14941  iscnp3 14946  trhom 14983  cntrsetlem 14999  aidm2 15097  dmrngcmp 15098  dualalg 15131  dualded 15132  dualcat2 15133  ishoma 15136  ishomb 15137  ismona 15158  isepia 15168  cinvlem1 15176  cinvlem2 15177  isfuna 15182  idfisf 15189  issubcat 15193  idsubfun 15206  infemb 15207  tarax3d4 15227  vtarsu 15263  tartarmap 15265  trclval 15271  fictblem 15370  fictb 15371  ordisoOLD 15374  hartoglemOLD 15383  omsubsucOLD 15386  omsubsuc2OLD 15387  omsubsdomlem2OLD 15389  omsubsdomOLD 15390  omsubdomOLD 15391  omsubelOLD 15392  elomsubsdOLD 15394  omsublimOLD 15396  infenomsubOLD 15398  subntr 15425  compsub 15431  hscptsscld 15434  compfipin0lem 15435  alexsublem2 15438  alexsublem4 15440  alexsub 15441  2ndc1stc 15477  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  flimcls 15588  filclus 15605  fclsfnflim 15614  fcluscomplem 15620  fcluscomp 15621  sfclusf 15624  tailmap 15636  tailuni 15638  tailfb 15639  filnetlem5 15644  filnet 15645  fnopabco 15711  upixp 15729  ac6gf 15749  indexdom 15754  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  fdc1 15813  fsumltisumii 15822  fsumltisumi 15823  fsumleisumii 15825  neificl 15841  mettrifi 15847  geomcau 15849  heiborlem1 15955  heiborlem2 15956  heiborlem4 15958  heiborlem8 15962  heiborlem23 15977  heiborlem33 15987  bfplem3 16000  bfplem8 16005  rrnmval 16014  rrndm 16015  rrnmet 16016  rrncms 16019  rrntotbndlem2 16021  grpkerinj 16042  phtpyid 16049  phtpycolem3 16053  phtpycolem4 16054  reparphtlem1 16063  reparphtlem2 16064  pcoval1 16074  pcoval2 16075  pcocn 16076  pcopt 16084  pcoass 16085  pcorev 16087  elpi1 16089  pi1f 16093  pi1val 16094  pi1gp 16095  isringd 16097  isdivrng1 16109  isdivrng2 16111  rnghomval 16118  isrnghom 16119  iscring2 16146  idlval 16161  isidl 16162  0idl 16173  0ring 16175  divrngidl 16176  intidl 16177  keridl 16180  pridlval 16181  maxidlval 16187  smprngpr 16200  igenval 16209  fveqsb 16431  smoiso 16453  addrcom 16475  strcval 16732  isposNEW 16773  pltval 16781  pgeval 16794  lubfval 16803  lubval 16804  lubprop 16805  glbfval 16808  glbval 16809  glbprop 16810  glbprople 16812  joinfval 16814  joinval 16815  joinlem 16817  meetfval 16821  meetval 16822  meetlem 16824  p0val 16843  p1val 16844  clatlem 16889  isopos 16909  cmtfval 16937  cvrfval 16987  patoms 17000  glbcon 17028  glbconx 17029  isgrpNEW 17104  grpinvfvalNEW 17125  isringNEW 17142  divrngmclNEW 17164  divrngidlemNEW 17165  divrngidNEW 17166  invrfval 17170  invrcl 17171  issrng 17176  islvec 17188  isphil 17195  plusssfval 17204  plusssval 17205  ocvfval 17206  ocvval 17207  csubspset 17208  iscsubsp 17209  lineset 17219  isline 17220  pointset 17222  psubspset 17225  ispsubsp 17226  pmapfval 17236  pmapval 17237  paddfval 17258  paddval 17259  polfval 17317  polval 17318  psubclset 17346  ispsubcl 17347  watomfval 17392  watomval 17393  pautset 17395  ispaut 17396  dilfset 17401  dilset 17402  trnfset 17404  trnset 17405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-uni 3178  df-fv 4014

Copyright terms: Public domain