Theorem fvex 3723

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 3193	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 1916	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 2505	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 1809	. . . . . . . 8 |- x e. V
5	4	unisn 2512	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1521	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1416	. . . . 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 2761	. . . 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 2865	. 2 |- U.{x | (F"{A}) = {x}} e. V
12	1, 11	eqeltr 1541	1 |- (F` A) e. V

Syntax hints:   = wceq 954   e. wcel 956  E*wmo 1379  {cab 1461  Vcvv 1807  {csn 2405  U.cuni 2498  "cima 3168  ` cfv 3177

This theorem is referenced by:  tz6.12i 3732  fnopabfv 3749  fvelrnb 3751  funimass4 3754  fvelimab 3756  fniinfv 3757  funfv 3761  dmfco 3764  fvco 3765  funfvop 3794  fvimacnvi 3795  fvimacnv 3796  funconstss 3799  fvimacnvALT 3800  fvelrn 3803  dff2 3808  fsn2 3827  fnressn 3828  funfvima3 3845  fvresex 3848  fniunfv 3856  funiunfv 3857  elunirnALT 3860  f1fv 3865  isomin 3890  isoini 3891  f1oiso 3895  tfrlem10 3911  tfrlem11 3912  tz7.44lem1 3918  tz7.44-2 3920  rdgsucopab 3937  rdglim2a 3941  frsucopab 3945  abianfplem 3952  oprex 3974  elxp7 4093  xpopth 4096  2ndrn 4100  dfopab2 4103  dfoprab3 4104  dfoprab5 4105  elopabi 4107  eloprabi 4108  foprab2 4109  fnoa 4138  fnom 4139  oav 4140  omv 4141  oev 4143  en1 4413  mapsnen 4416  xpdom2 4428  pw2en 4432  mapxpen 4481  xpmapenlem4 4485  xpmapenlem5 4486  phplem4 4497  unifi 4538  fiint 4540  fodomfi 4546  inf0 4586  inf3lemd 4592  inf3lem1 4593  inf3lem2 4594  inf3lem3 4595  inf3lem6 4598  trcl 4625  tz9.1 4626  r1suc 4632  r1ord 4635  rankval2 4650  rankr1 4654  bndrank 4662  rankuni2 4670  rankr1id 4677  rankuni 4678  rankr1b 4679  rankval4 4682  rankelun 4687  rankxpsuc 4695  scott0 4697  aceq3lem 4712  aceq4 4714  aceq5 4720  aceq6b 4722  numthlem 4763  unidom 4788  oncardon 4800  oncardid 4801  cardon 4807  cardid 4808  oncard 4809  sdomsdomcard 4828  cardidm 4829  ondomon 4836  cardiun 4839  cardprc 4841  alephon 4845  alephsuc 4846  alephcard 4847  alephsucpw 4850  aleph1 4851  alephordi 4854  alephsucdom 4860  cardaleph 4865  alephiso 4872  alephfplem1 4876  alephfplem2 4877  alephval3 4883  cflem 4885  cardcf 4891  cflecard 4892  cda1en 4906  recidpq 5051  recclpq 5052  recrecpq 5053  dmrecpq 5054  ltrpq 5065  1pr 5097  addclprlem1 5098  addclprlem2 5099  mulclprlem 5101  1idpr 5113  prlem936a 5133  prlem936 5135  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  reclem4pr 5139  seq1lem1 6254  seq1fnlem 6258  seq1val2 6259  seq11lem 6260  seq1suclem 6261  shftfn 6288  shftvalt 6291  seqzres2 6501  serzcl1 6502  expvalt 6510  absvalt 6702  sumex 6927  sumeq2 6931  fsumserz2 6949  serzfsum 6950  serzref 6997  serz0 6999  serzcmp0 7001  serzmulc 7004  climconst3 7041  climsub 7074  climcmplem 7081  climcmpc1 7083  iserzcmp0 7087  caucvg3 7111  iserzabslem 7122  iserzabs 7123  cvgcmp3ce 7131  isumval2t 7138  isumclim3t 7143  isumclim4t 7144  isum1p 7149  isummulc1 7155  isummulc1ALT 7156  isumcmpi 7158  isumsplit 7159  cvgratlem3ALT 7192  cvgratlem3 7195  efseq0ex 7261  efclt 7262  ef0 7285  efcj 7286  efaddlem26 7313  efaddlem28 7315  eftlexOLD 7327  effsumle 7346  efm1lim 7359  eflegeolem2 7362  acdc3lem 7436  acdclem 7444  acdcALT 7446  aleph1re 7502  infmap2lem1 7529  alephadd 7532  alephmul 7533  alephexp1 7534  alephsuc3 7535  alephexp2 7536  gch-kn 7537  tgclt 7574  lpval 7693  opntop 7822  lmfex 7910  metcnp4lem1 7918  xplmi 7923  xplmi2 7924  xplm 7925  xpcn 7926  oprcn 7927  bopcnlem1 7931  bopcnlem2 7932  bopcnlem4 7934  addcn 7936  subcn 7937  mulcn 7938  fsumcnlem 7939  bafval 8175  nvvop 8180  imsval 8267  imsmetlem 8274  sqcn 8283  ipfval 8299  ip1cnilem2 8321  ip1cnilem3 8322  sspval 8329  lnoval 8360  islno 8361  nmofval 8370  nmoval 8371  nmosetn0 8373  nmolb 8379  0ofval 8392  0oval 8393  0oo 8394  nmlno0lem 8398  blocni 8409  ajfval 8413  isph 8425  phpar 8427  ubthlem1 8473  ubthlem3 8475  ubthlem6 8478  minveclem31 8519  minveclem33 8521  minveceu 8527  hlex 8543  htthlem11 8573  efgh 8652  efghgrpilem 8653  efif 8655  efifo 8663  efif1 8671  shftefif1olem 8680  eff1i 8683  effoi 8684  normvalt 8929  projlem23 9147  projlem31 9155  hsupclt 9245  sshjvalt 9258  sshjval3t 9264  pjspansnt 9440  nmopsetn0 9732  nmfnsetn0 9745  eigvalvalt 9763  nmoplbt 9771  nmfnlbt 9787  adjt 9796  nmlnop0ALT 9858  nmcopexlem1 9889  nmcfnexlem1 9918  branmfnt 9976  hstrlem2 10124  atoml 10246  neifil 10478  eloi 10539  aidm 10563  aidmold 10564  ishoma 10595  ishomb 10596  ismona 10615  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-uni 2499  df-fv 3193

Copyright terms: Public domain