Theorem fvex 3671

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 3161	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2		moeq 1892	. . . . 5 |- E*x x = U.(F"{A})
3		unieq 2478	. . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4		visset 1788	. . . . . . . 8 |- x e. V
5	4	unisn 2485	. . . . . . 7 |- U.{x} = x
6	3, 5	syl6req 1500	. . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
7	6	immoi 1395	. . . . 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 2734	. . . 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 2834	. 2 |- U.{x | (F"{A}) = {x}} e. V
12	1, 11	eqeltr 1520	1 |- (F` A) e. V

Syntax hints:   = wceq 1099   e. wcel 1105  E*wmo 1358  {cab 1440  Vcvv 1786  {csn 2380  U.cuni 2471  "cima 3136  ` cfv 3145

This theorem is referenced by:  tz6.12i 3680  fnopabfv 3697  fvelrnb 3699  funimass4 3702  fvelimab 3704  fniinfv 3705  funfv 3709  dmfco 3712  fvco 3713  funfvop 3742  fvimacnvi 3743  fvimacnv 3744  funconstss 3747  fvimacnvALT 3748  fvelrn 3751  dff2 3756  fsn2 3775  fnressn 3776  funfvima3 3793  fvresex 3796  fniunfv 3804  funiunfv 3805  elunirnALT 3808  f1fv 3813  isomin 3838  isoini 3839  f1oiso 3843  tfrlem10 3859  tfrlem11 3860  tz7.44lem1 3866  tz7.44-2 3868  rdgsucopab 3885  rdglim2a 3889  frsucopab 3893  abianfplem 3900  oprex 3922  elxp7 4041  xpopth 4044  2ndrn 4048  dfopab2 4051  dfoprab3 4052  dfoprab5 4053  elopabi 4055  eloprabi 4056  foprab2 4057  fnoa 4086  fnom 4087  oav 4088  omv 4089  oev 4091  en1 4361  mapsnen 4364  xpdom2 4376  pw2en 4380  mapxpen 4427  xpmapenlem4 4431  xpmapenlem5 4432  phplem4 4443  unifi 4484  fiint 4486  fodomfi 4492  inf0 4530  inf3lemd 4536  inf3lem1 4537  inf3lem2 4538  inf3lem3 4539  inf3lem6 4542  trcl 4569  tz9.1 4570  r1suc 4576  r1ord 4579  rankval2 4594  rankr1 4598  bndrank 4606  rankuni2 4614  rankr1id 4621  rankuni 4622  rankr1b 4623  rankval4 4626  rankelun 4631  rankxpsuc 4639  scott0 4641  aceq3lem 4656  aceq4 4658  aceq5 4664  aceq6b 4666  numthlem 4707  unidom 4732  oncardon 4744  oncardid 4745  cardon 4751  cardid 4752  oncard 4753  sdomsdomcard 4771  cardidm 4772  ondomon 4779  cardiun 4782  cardprc 4784  alephon 4788  alephsuc 4789  alephcard 4790  alephsucpw 4793  aleph1 4794  alephordi 4797  alephsucdom 4803  cardaleph 4808  alephiso 4815  alephfplem1 4819  alephfplem2 4820  alephval3 4826  cflem 4828  cardcf 4834  cflecard 4835  cda1en 4849  recidpq 4994  recclpq 4995  recrecpq 4996  dmrecpq 4997  ltrpq 5008  1pr 5040  addclprlem1 5041  addclprlem2 5042  mulclprlem 5044  1idpr 5056  prlem936a 5076  prlem936 5078  reclem1pr 5079  reclem2pr 5080  reclem3pr 5081  reclem4pr 5082  seq1lem1 6197  seq1fnlem 6201  seq1val2 6202  seq11lem 6203  seq1suclem 6204  shftfn 6231  shftvalt 6234  seqzres2 6444  serzcl1 6445  expvalt 6453  absvalt 6645  sumex 6870  sumeq2 6874  fsumserz2 6892  serzfsum 6893  serzref 6940  serz0 6942  serzcmp0 6944  serzmulc 6947  climconst3 6984  climsub 7017  climcmplem 7024  climcmpc1 7026  iserzcmp0 7030  caucvg3 7054  iserzabslem 7065  iserzabs 7066  cvgcmp3ce 7074  isumval2t 7081  isumclim3t 7086  isumclim4t 7087  isum1p 7092  isummulc1 7098  isummulc1ALT 7099  isumcmpi 7101  isumsplit 7102  cvgratlem3ALT 7135  cvgratlem3 7138  efseq0ex 7204  efclt 7205  ef0 7228  efcj 7229  efaddlem26 7256  efaddlem28 7258  eftlexOLD 7270  effsumle 7289  efm1lim 7302  eflegeolem2 7305  acdc3lem 7379  acdclem 7387  acdcALT 7389  aleph1re 7445  infmap2lem1 7472  alephadd 7475  alephmul 7476  alephexp1 7477  alephsuc3 7478  alephexp2 7479  gch-kn 7480  tgclt 7517  lpval 7632  opntop 7758  lmfex 7842  metcnp4lem1 7850  xplmi 7855  xplmi2 7856  xplm 7857  xpcn 7858  oprcn 7859  bopcnlem1 7863  bopcnlem2 7864  bopcnlem4 7866  addcn 7868  subcn 7869  mulcn 7870  fsumcnlem 7871  bafval 8103  nvvop 8108  imsval 8191  imsmetlem 8198  sqcn 8207  ipfval 8221  ip1cnilem2 8243  ip1cnilem3 8244  sspval 8251  lnoval 8282  islno 8283  nmofval 8292  nmoval 8293  nmosetn0 8295  nmolb 8301  0ofval 8314  0oval 8315  0oo 8316  nmlno0lem 8320  blocni 8331  ajfval 8335  isph 8347  phpar 8349  ubthlem1 8395  ubthlem3 8397  ubthlem6 8400  minveclem31 8441  minveclem33 8443  minveceu 8449  hlex 8464  htthlem11 8494  efgh 8546  efghgrpilem 8547  efif 8549  efifo 8557  efif1 8565  shftefif1olem 8574  shftefif1olemOLD 8575  eff1i 8578  effoi 8579  effoiOLD 8580  neifil 8792  eloi 8853  aidm 8877  aidmold 8878  ishoma 8909  ishomb 8910  ismona 8929  isfuna 8940  normvalt 9139  projlem23 9338  projlem31 9346  hsupclt 9436  sshjvalt 9449  sshjval3t 9455  pjspansnt 9631  nmopsetn0 9923  nmfnsetn0 9936  eigvalvalt 9954  nmoplbt 9962  nmfnlbt 9978  adjt 9987  nmlnop0ALT 10049  nmcopexlem1 10080  nmcfnexlem1 10109  branmfnt 10165  hstrlem2 10310  atoml 10431

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-uni 2472  df-fv 3161

Copyright terms: Public domain