Theorem fvex 3732

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 3198	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 1920	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 2510	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 1813	. . . . . . . 8 |- x e. V
5	4	unisn 2517	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1524	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1418	. . . . 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 2766	. . . 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 2870	. 2 |- U.{x | (F"{A}) = {x}} e. V
12	1, 11	eqeltr 1544	1 |- (F` A) e. V

Syntax hints:   = wceq 956   e. wcel 958  E*wmo 1381  {cab 1463  Vcvv 1811  {csn 2409  U.cuni 2503  "cima 3173  ` cfv 3182

This theorem is referenced by:  tz6.12i 3741  fnopabfv 3758  fvelrnb 3760  funimass4 3763  fvelimab 3765  fniinfv 3766  funfv 3770  dmfco 3773  fvco 3774  funfvop 3803  fvimacnvi 3804  fvimacnv 3805  funconstss 3808  fvimacnvALT 3809  fvelrn 3812  dff2 3817  fsn2 3836  fnressn 3837  funfvima3 3854  fvresex 3857  fniunfv 3865  funiunfv 3866  elunirnALT 3869  f1fv 3874  isomin 3899  isoini 3900  f1oiso 3904  tfrlem10 3920  tfrlem11 3921  tz7.44lem1 3927  tz7.44-2 3929  rdgsucopab 3946  rdglim2a 3950  frsucopab 3954  abianfplem 3961  oprex 3983  elxp7 4103  xpopth 4106  2ndrn 4110  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  elopabi 4117  eloprabi 4118  foprab2 4119  fnoa 4148  fnom 4149  oav 4150  omv 4151  oev 4153  en1 4425  mapsnen 4428  xpdom2 4440  pw2en 4444  mapxpen 4493  xpmapenlem4 4497  xpmapenlem5 4498  phplem4 4509  unifi 4550  fiint 4552  fodomfi 4558  inf0 4598  inf3lemd 4604  inf3lem1 4605  inf3lem2 4606  inf3lem3 4607  inf3lem6 4610  trcl 4637  tz9.1 4638  r1suc 4644  r1ord 4647  rankval2 4662  rankr1 4666  bndrank 4674  rankuni2 4682  rankr1id 4689  rankuni 4690  rankr1b 4691  rankval4 4694  rankelun 4699  rankxpsuc 4707  scott0 4709  aceq3lem 4724  aceq4 4726  aceq5 4732  aceq6b 4734  numthlem 4775  unidom 4800  oncardon 4812  oncardid 4813  cardon 4819  cardid 4820  oncard 4821  sdomsdomcard 4840  cardidm 4841  ondomon 4848  cardiun 4851  cardprc 4853  alephon 4857  alephsuc 4858  alephcard 4859  alephsucpw 4862  aleph1 4863  alephordi 4866  alephsucdom 4872  cardaleph 4877  alephiso 4884  alephfplem1 4888  alephfplem2 4889  alephval3 4895  cflem 4897  cardcf 4903  cflecard 4904  cda1en 4918  recidpq 5063  recclpq 5064  recrecpq 5065  dmrecpq 5066  ltrpq 5077  1pr 5109  addclprlem1 5110  addclprlem2 5111  mulclprlem 5113  1idpr 5125  prlem936a 5145  prlem936 5147  reclem1pr 5148  reclem2pr 5149  reclem3pr 5150  reclem4pr 5151  seq1lem1 6295  seq1fnlem 6299  seq1val2 6300  seq11lem 6301  seq1suclem 6302  shftfn 6329  shftvalt 6332  seqzres2 6547  serzcl1 6548  expvalt 6556  absvalt 6748  sumex 6966  sumeq2 6970  fsumserz2 6988  serzfsum 6989  serzref 7036  serz0 7038  serzcmp0 7040  serzmulc 7043  climconst3 7081  climsub 7115  climcmplem 7122  climcmpc1 7124  iserzcmp0 7128  caucvg3 7152  iserzabslem 7163  iserzabs 7164  cvgcmp3ce 7172  isumval2t 7179  isumclim3t 7185  isumclim4t 7186  isum1p 7191  isummulc1 7197  isummulc1ALT 7198  isumcmpi 7200  isumsplit 7201  cvgratlem3ALT 7234  cvgratlem3 7237  efseq0ex 7296  efclt 7297  ef0 7320  efcj 7321  efaddlem26 7348  efaddlem28 7350  eftlexOLD 7362  effsumle 7382  efm1lim 7396  eflegeolem2 7399  acdc3lem 7471  acdclem 7479  acdcALT 7481  aleph1re 7536  infmap2lem1 7564  alephadd 7567  alephmul 7568  alephexp1 7569  alephsuc3 7570  alephexp2 7571  gch-kn 7572  tgclt 7609  lpval 7728  opntop 7855  lmfex 7944  metcnp4lem1 7953  xplmi 7958  xplmi2 7959  xplm 7960  xpcn 7961  oprcn 7962  bopcnlem1 7966  bopcnlem2 7967  bopcnlem4 7969  addcn 7971  subcn 7972  mulcn 7973  fsumcnlem 7974  bafval 8208  nvvop 8213  imsval 8301  imsmetlem 8308  sqcn 8320  ipfval 8337  ip1cnilem2 8359  ip1cnilem3 8360  sspval 8367  lnoval 8398  islno 8399  nmofval 8410  nmoval 8411  nmosetn0 8413  nmolb 8419  0ofval 8432  0oval 8433  0oo 8434  nmlno0lem 8438  lnon0 8443  blocni 8450  ajfval 8454  isph 8466  phpar 8468  ubthlem1 8514  ubthlem3 8516  ubthlem6 8519  minveclem31 8560  minveclem33 8562  minveceu 8568  hlex 8585  htthlem11 8615  efgh 8703  efghgrpilem 8704  efif 8706  efifo 8714  efif1 8722  shftefif1olem 8726  eff1i 8729  effoi 8730  normvalt 8975  projlem23 9193  projlem31 9201  hsupclt 9292  sshjvalt 9305  sshjval3t 9311  pjspansnt 9485  nmopsetn0 9777  nmfnsetn0 9790  eigvalvalt 9808  nmoplbt 9816  nmfnlbt 9833  adjt 9842  nmlnop0ALT 9905  nmcopexlem1 9936  nmcfnexlem1 9965  branmfnt 10023  hstrlem2 10171  atoml 10294  neifil 10527  eloi 10602  aidm 10626  aidmold 10627  ishoma 10658  ishomb 10659  ismona 10678  isfuna 10691  idfisf 10697

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-uni 2504  df-fv 3198

Copyright terms: Public domain