HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem fvex 3717
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
StepHypRef Expression
1 df-fv 3188 . 2 |- (F` A) = U.{x | (F"{A}) = {x}}
2 moeq 1911 . . . . 5 |- E*x x = U.(F"{A})
3 unieq 2500 . . . . . . 7 |- ((F"{A}) = {x} -> U.(F"{A}) = U.{x})
4 visset 1804 . . . . . . . 8 |- x e. V
54unisn 2507 . . . . . . 7 |- U.{x} = x
63, 5syl6req 1516 . . . . . 6 |- ((F"{A}) = {x} -> x = U.(F"{A}))
76immoi 1411 . . . . 5 |- (E*x x = U.(F"{A}) -> E*x(F"{A}) = {x})
82, 7ax-mp 7 . . . 4 |- E*x(F"{A}) = {x}
9 moabex 2756 . . . 4 |- (E*x(F"{A}) = {x} -> {x | (F"{A}) = {x}} e. V)
108, 9ax-mp 7 . . 3 |- {x | (F"{A}) = {x}} e. V
1110uniex 2861 . 2 |- U.{x | (F"{A}) = {x}} e. V
121, 11eqeltr 1536 1 |- (F` A) e. V
Colors of variables: wff set class
Syntax hints:   = wceq 953   e. wcel 955  E*wmo 1374  {cab 1456  Vcvv 1802  {csn 2399  U.cuni 2493  "cima 3163  ` cfv 3172
This theorem is referenced by:  tz6.12i 3726  fnopabfv 3743  fvelrnb 3745  funimass4 3748  fvelimab 3750  fniinfv 3751  funfv 3755  dmfco 3758  fvco 3759  funfvop 3788  fvimacnvi 3789  fvimacnv 3790  funconstss 3793  fvimacnvALT 3794  fvelrn 3797  dff2 3802  fsn2 3821  fnressn 3822  funfvima3 3839  fvresex 3842  fniunfv 3850  funiunfv 3851  elunirnALT 3854  f1fv 3859  isomin 3884  isoini 3885  f1oiso 3889  tfrlem10 3905  tfrlem11 3906  tz7.44lem1 3912  tz7.44-2 3914  rdgsucopab 3931  rdglim2a 3935  frsucopab 3939  abianfplem 3946  oprex 3968  elxp7 4087  xpopth 4090  2ndrn 4094  dfopab2 4097  dfoprab3 4098  dfoprab5 4099  elopabi 4101  eloprabi 4102  foprab2 4103  fnoa 4132  fnom 4133  oav 4134  omv 4135  oev 4137  en1 4407  mapsnen 4410  xpdom2 4422  pw2en 4426  mapxpen 4475  xpmapenlem4 4479  xpmapenlem5 4480  phplem4 4491  unifi 4532  fiint 4534  fodomfi 4540  inf0 4578  inf3lemd 4584  inf3lem1 4585  inf3lem2 4586  inf3lem3 4587  inf3lem6 4590  trcl 4617  tz9.1 4618  r1suc 4624  r1ord 4627  rankval2 4642  rankr1 4646  bndrank 4654  rankuni2 4662  rankr1id 4669  rankuni 4670  rankr1b 4671  rankval4 4674  rankelun 4679  rankxpsuc 4687  scott0 4689  aceq3lem 4704  aceq4 4706  aceq5 4712  aceq6b 4714  numthlem 4755  unidom 4780  oncardon 4792  oncardid 4793  cardon 4799  cardid 4800  oncard 4801  sdomsdomcard 4820  cardidm 4821  ondomon 4828  cardiun 4831  cardprc 4833  alephon 4837  alephsuc 4838  alephcard 4839  alephsucpw 4842  aleph1 4843  alephordi 4846  alephsucdom 4852  cardaleph 4857  alephiso 4864  alephfplem1 4868  alephfplem2 4869  alephval3 4875  cflem 4877  cardcf 4883  cflecard 4884  cda1en 4898  recidpq 5043  recclpq 5044  recrecpq 5045  dmrecpq 5046  ltrpq 5057  1pr 5089  addclprlem1 5090  addclprlem2 5091  mulclprlem 5093  1idpr 5105  prlem936a 5125  prlem936 5127  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  reclem4pr 5131  seq1lem1 6246  seq1fnlem 6250  seq1val2 6251  seq11lem 6252  seq1suclem 6253  shftfn 6280  shftvalt 6283  seqzres2 6493  serzcl1 6494  expvalt 6502  absvalt 6694  sumex 6919  sumeq2 6923  fsumserz2 6941  serzfsum 6942  serzref 6989  serz0 6991  serzcmp0 6993  serzmulc 6996  climconst3 7033  climsub 7066  climcmplem 7073  climcmpc1 7075  iserzcmp0 7079  caucvg3 7103  iserzabslem 7114  iserzabs 7115  cvgcmp3ce 7123  isumval2t 7130  isumclim3t 7135  isumclim4t 7136  isum1p 7141  isummulc1 7147  isummulc1ALT 7148  isumcmpi 7150  isumsplit 7151  cvgratlem3ALT 7184  cvgratlem3 7187  efseq0ex 7253  efclt 7254  ef0 7277  efcj 7278  efaddlem26 7305  efaddlem28 7307  eftlexOLD 7319  effsumle 7338  efm1lim 7351  eflegeolem2 7354  acdc3lem 7428  acdclem 7436  acdcALT 7438  aleph1re 7494  infmap2lem1 7521  alephadd 7524  alephmul 7525  alephexp1 7526  alephsuc3 7527  alephexp2 7528  gch-kn 7529  tgclt 7566  lpval 7684  opntop 7810  lmfex 7894  metcnp4lem1 7902  xplmi 7907  xplmi2 7908  xplm 7909  xpcn 7910  oprcn 7911  bopcnlem1 7915  bopcnlem2 7916  bopcnlem4 7918  addcn 7920  subcn 7921  mulcn 7922  fsumcnlem 7923  bafval 8161  nvvop 8166  imsval 8254  imsmetlem 8261  sqcn 8270  ipfval 8286  ip1cnilem2 8308  ip1cnilem3 8309  sspval 8316  lnoval 8347  islno 8348  nmofval 8357  nmoval 8358  nmosetn0 8360  nmolb 8366  0ofval 8379  0oval 8380  0oo 8381  nmlno0lem 8385  blocni 8396  ajfval 8400  isph 8412  phpar 8414  ubthlem1 8460  ubthlem3 8462  ubthlem6 8465  minveclem31 8506  minveclem33 8508  minveceu 8514  hlex 8530  htthlem11 8560  efgh 8633  efghgrpilem 8634  efif 8636  efifo 8644  efif1 8652  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  effoi 8666  effoiOLD 8667  normvalt 8911  projlem23 9124  projlem31 9132  hsupclt 9222  sshjvalt 9235  sshjval3t 9241  pjspansnt 9417  nmopsetn0 9709  nmfnsetn0 9722  eigvalvalt 9740  nmoplbt 9748  nmfnlbt 9764  adjt 9773  nmlnop0ALT 9835  nmcopexlem1 9866  nmcfnexlem1 9895  branmfnt 9951  hstrlem2 10096  atoml 10217  neifil 10442  eloi 10503  aidm 10527  aidmold 10528  ishoma 10559  ishomb 10560  ismona 10579  isfuna 10592
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-un 2857
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-uni 2494  df-fv 3188
Copyright terms: Public domain