Theorem fvex 3843

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 3279	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 1966	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 2576	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 1859	. . . . . . . 8 |- x e. V
5	4	unisn 2583	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1567	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1457	. . . . 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 2844	. . . 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 3093	. 2 |- U.{x | (F"{A}) = {x}} e. V
12	1, 11	eqeltri 1587	1 |- (F` A) e. V

Syntax hints:   = wceq 992   e. wcel 994  E*wmo 1420  {cab 1505  Vcvv 1857  {csn 2467  U.cuni 2569  "cima 3254  ` cfv 3263

This theorem is referenced by:  tz6.12i 3852  dffn5 3869  fvelrnb 3871  funimass4 3874  fvelimab 3876  fniinfv 3877  funfv 3881  dmfco 3884  fvco 3885  funfvop 3917  fvimacnvi 3918  fvimacnv 3919  funconstss 3922  fvimacnvALT 3923  fvelrn 3926  dff3 3931  fsn2 3950  fnressn 3951  funfvima3 3968  fvresex 3971  fniunfv 3979  funiunfv 3980  elunirnALT 3983  dff13 3988  isomin 4013  isoini 4014  f1oiso 4018  oprex 4041  elxp7 4162  xpopth 4166  2ndrn 4170  dfopab2 4173  dfoprab3 4174  dfoprab3s 4175  elopabi 4179  eloprabi 4180  foprab2 4181  iunfoprab 4192  fparlem1 4199  fparlem2 4200  fpar 4203  tfrlem10 4221  tfrlem11 4222  tz7.44lem1 4228  tz7.44-2 4230  rdgsucopab 4247  rdglim2a 4251  frsucopab 4255  abianfplem 4262  fnoa 4284  fnom 4285  oav 4286  omv 4287  oev 4289  en1 4567  mapsnen 4570  xpdom2 4583  pw2en 4587  ac6sfilem3 4590  ac6sfi 4591  mapxpen 4642  xpmapenlem4 4646  xpmapenlem5 4647  phplem4 4658  unifi 4701  fiint 4703  fodomfi 4709  inf0 4751  inf3lemd 4757  inf3lem1 4758  inf3lem2 4759  inf3lem3 4760  inf3lem6 4763  trcl 4791  tz9.1 4792  r1suc 4798  r1ord 4801  rankval2 4816  rankr1 4820  bndrank 4828  rankuni2 4836  rankr1id 4843  rankuni 4844  rankr1b 4845  rankval4 4848  rankelun 4853  rankxpsuc 4861  scott0 4863  aceq3lem 4878  aceq4 4880  aceq5 4886  aceq6b 4888  numthlem 4929  unidom 4954  oncardon 4966  oncardid 4967  cardon 4974  cardid 4975  oncard 4976  unsnen 4983  sdomsdomcard 4998  cardidm 4999  ondomon 5006  cardiun 5009  cardprc 5011  alephon 5015  alephsuc 5016  alephcard 5017  alephsucpw 5020  aleph1 5021  alephordi 5024  alephsucdom 5030  cardaleph 5035  alephiso 5042  alephfplem1 5046  alephfplem2 5047  alephval3 5053  cflem 5055  cardcf 5061  cflecard 5062  cda1en 5078  nnaun 5091  recidpq 5225  recclpq 5226  recrecpq 5227  dmrecpq 5228  ltrpq 5239  1pr 5271  addclprlem1 5272  addclprlem2 5273  mulclprlem 5275  1idpr 5287  prlem936a 5307  prlem936 5309  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  reclem4pr 5313  cardfz 6671  seq1lem1 6674  seq1fnlem 6678  seq1val2 6679  seq11lem 6680  seq1suclem 6681  shftfn 6708  shftval 6711  seqzres2 6756  serzcl1i 6757  expval 6765  absval 6963  sumex 7184  sumeq2 7188  fsumserz2 7206  serzfsum 7207  serzrefi 7254  serz0 7256  serzcmp0 7258  serzmulci 7261  climconst3 7299  climsub 7333  climcmplem 7340  climcmpc1 7342  iserzcmp0 7346  caucvg3i 7370  iserzabslem 7381  iserzabsi 7382  cvgcmp3cei 7391  isumval2 7398  isumclim3 7404  isumclim4 7405  isum1p 7410  isummulc1 7416  isummulc1iALT 7417  isumcmpii 7419  isumspliti 7420  explecnv 7438  cvgratlem3ALT 7454  cvgratlem3 7457  efseq0ex 7516  efcl 7517  ef0 7540  efcji 7541  efaddlem26 7568  efaddlem28 7570  eftlexiOLD 7582  effsumlei 7605  efm1limi 7619  eflegeolem2 7622  acdc3lem 7697  acdclem 7706  acdcALT 7708  aleph1re 7763  infmap2lem1 7791  alephadd 7794  alephmul 7795  alephexp1 7796  alephsuc3 7797  alephexp2 7798  gch-kn 7799  tgcl 7836  lpval 7953  opntop 8080  lmfex 8170  metcnp4lem1 8179  xplmi 8184  xplmi2 8185  xplm 8186  xpcn 8187  oprcn 8188  bopcnlem1 8192  bopcnlem2 8193  bopcnlem4 8195  addcn 8197  subcn 8198  mulcn 8199  fsumcnlem 8200  gxval 8314  bafval 8470  nvvop 8475  imsval 8563  imsmetlem 8570  vacnlem4 8585  vacnlem5 8586  vacnlem6 8587  sqcn 8589  ipfval 8606  ip1cnilem2 8628  ip1cnilem3 8629  sspval 8636  lnoval 8667  islno 8668  nmofval 8679  nmoval 8680  nmosetn0 8682  nmolb 8688  0ofval 8702  0oval 8703  0oo 8704  nmlno0lem 8708  lnon0 8713  blocni 8720  ajfval 8724  isph 8737  phpar 8739  ajval 8778  ubthlem1 8787  ubthlem3 8789  ubthlem6 8792  minveclem31 8835  minveclem33 8837  minveceu 8843  hlex 8862  htthlem11 8892  efgh 8990  efghgrpilem 8991  efif 8993  efifo 9001  efif1 9009  shftefif1olem 9013  eff1i 9016  effoi 9017  normval 9266  projlem23 9484  projlem31 9492  hsupcl 9583  sshjval 9596  sshjval3 9602  pjspansn 9776  nmopsetn0 10072  nmfnsetn0 10085  eigvalval 10103  nmoplb 10111  nmfnlb 10128  adj1 10137  nmlnop0iALT 10199  nmcopexlem1 10230  nmcfnexlem1 10259  branmfn 10317  branmfnOLD 10318  hstrlem2 10467  atomli 10591  prj1 10809  eloi 10817  seqzp2 10918  expmiz 10936  expm 10937  unmnd 10951  rngunval2 10965  dvrunz 10970  neifil 11080  aidm2 11204  dmrngcmp 11205  ishoma 11242  ishomb 11243  ismona 11264  isepia 11274  cinvlem1 11282  cinvlem2 11283  isfuna 11288  idfisf 11295  issubcat 11299  idsubfun 11312  infemb 11313  fictblem 11422  fictb 11423  ordiso 11426  hartoglem 11435  omsubsuc 11438  omsubsuc2 11439  omsubsdomlem2 11441  omsubsdom 11442  omsubdom 11443  omsubel 11444  elomsubsd 11446  omsublim 11448  infenomsub 11450  cnpnei 11472  subntr 11482  compsub 11488  hscptsscld 11491  compfipin0lem 11492  alexsublem2 11497  alexsublem4 11499  alexsub 11500  2ndc1stc 11538  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  fbssint 11626  fsubbas 11630  fgfil 11638  flimcls 11684  hausfillim 11685  isfilmap 11689  sflimf 11708  filclus 11717  fclsfnflim 11726  fcluscomplem 11732  fcluscomp 11733  sfclusf 11736  tailmap 11759  tailuni 11761  tailfb 11762  filnetlem5 11767  filnet 11768  gaid 11776  oprabopabf 11807  fnopabco 11810  oprabco 11811  upxp 11822  upixp 11823  dif1en 11833  ac6gf 11841  indexd 11846  sdclem1 11875  sdclem2 11876  sdc 11877  fsumltisumii 11885  fsumltisumi 11886  fsumleisumii 11888  neificl 11904  mettrifi 11912  geomcau 11914  txval 11972  uptx 11978  txcnopab 11980  heiborlem1 12011  heiborlem2 12012  heiborlem4 12014  heiborlem8 12018  heiborlem23 12033  heiborlem33 12043  bfplem3 12056  bfplem8 12061  rrnmval 12070  rrndm 12071  rrnmet 12072  rrncms 12075  rrntotbndlem2 12077  phtpyid 12091  phtpycolem3 12095  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-uni 2570  df-fv 3279

Copyright terms: Public domain