Theorem fvex 3734

Description: The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.

Assertion

Ref	Expression
fvex	⊢ (F ‘A) ∈ V

Proof of Theorem fvex

Step	Hyp	Ref	Expression
1		df-fv 3198	. 2 ⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}
2		moeq 1916	. . . . 5 ⊢ ∃*x x = ∪(F “ {A})
3		unieq 2506	. . . . . . 7 ⊢ ((F “ {A}) = {x} → ∪(F “ {A}) = ∪{x})
4		visset 1809	. . . . . . . 8 ⊢ x ∈ V
5	4	unisn 2513	. . . . . . 7 ⊢ ∪{x} = x
6	3, 5	syl6req 1521	. . . . . 6 ⊢ ((F “ {A}) = {x} → x = ∪(F “ {A}))
7	6	immoi 1416	. . . . 5 ⊢ (∃*x x = ∪(F “ {A}) → ∃*x(F “ {A}) = {x})
8	2, 7	ax-mp 7	. . . 4 ⊢ ∃*x(F “ {A}) = {x}
9		moabex 2762	. . . 4 ⊢ (∃*x(F “ {A}) = {x} → {x∣(F “ {A}) = {x}} ∈ V)
10	8, 9	ax-mp 7	. . 3 ⊢ {x∣(F “ {A}) = {x}} ∈ V
11	10	uniex 2869	. 2 ⊢ ∪{x∣(F “ {A}) = {x}} ∈ V
12	1, 11	eqeltr 1541	1 ⊢ (F ‘A) ∈ V

Syntax hints:   = wceq 954   ∈ wcel 956  ∃*wmo 1379  {cab 1461  Vcvv 1807  {csn 2405  ∪cuni 2499   “ cima 3173   ‘cfv 3182

This theorem is referenced by:  tz6.12i 3743  fnopabfv 3760  fvelrnb 3762  funimass4 3765  fvelimab 3767  fniinfv 3768  funfv 3772  dmfco 3775  fvco 3776  funfvop 3805  fvimacnvi 3806  fvimacnv 3807  funconstss 3810  fvimacnvALT 3811  fvelrn 3814  dff2 3819  fsn2 3838  fnressn 3839  funfvima3 3856  fvresex 3859  fniunfv 3867  funiunfv 3868  elunirnALT 3871  f1fv 3876  isomin 3901  isoini 3902  f1oiso 3906  tfrlem10 3922  tfrlem11 3923  tz7.44lem1 3929  tz7.44-2 3931  rdgsucopab 3948  rdglim2a 3952  frsucopab 3956  abianfplem 3963  oprex 3985  elxp7 4104  xpopth 4107  2ndrn 4111  dfopab2 4114  dfoprab3 4115  dfoprab5 4116  elopabi 4118  eloprabi 4119  foprab2 4120  fnoa 4149  fnom 4150  oav 4151  omv 4152  oev 4154  en1 4424  mapsnen 4427  xpdom2 4439  pw2en 4443  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 6266  seq1fnlem 6270  seq1val2 6271  seq11lem 6272  seq1suclem 6273  shftfn 6300  shftvalt 6303  seqzres2 6513  serzcl1 6514  expvalt 6522  absvalt 6714  sumex 6939  sumeq2 6943  fsumserz2 6961  serzfsum 6962  serzref 7009  serz0 7011  serzcmp0 7013  serzmulc 7016  climconst3 7053  climsub 7086  climcmplem 7093  climcmpc1 7095  iserzcmp0 7099  caucvg3 7123  iserzabslem 7134  iserzabs 7135  cvgcmp3ce 7143  isumval2t 7150  isumclim3t 7155  isumclim4t 7156  isum1p 7161  isummulc1 7167  isummulc1ALT 7168  isumcmpi 7170  isumsplit 7171  cvgratlem3ALT 7204  cvgratlem3 7207  efseq0ex 7273  efclt 7274  ef0 7297  efcj 7298  efaddlem26 7325  efaddlem28 7327  eftlexOLD 7339  effsumle 7358  efm1lim 7371  eflegeolem2 7374  acdc3lem 7448  acdclem 7456  acdcALT 7458  aleph1re 7514  infmap2lem1 7541  alephadd 7544  alephmul 7545  alephexp1 7546  alephsuc3 7547  alephexp2 7548  gch-kn 7549  tgclt 7586  lpval 7705  opntop 7834  lmfex 7922  metcnp4lem1 7930  xplmi 7935  xplmi2 7936  xplm 7937  xpcn 7938  oprcn 7939  bopcnlem1 7943  bopcnlem2 7944  bopcnlem4 7946  addcn 7948  subcn 7949  mulcn 7950  fsumcnlem 7951  bafval 8189  nvvop 8194  imsval 8283  imsmetlem 8290  sqcn 8299  ipfval 8315  ip1cnilem2 8337  ip1cnilem3 8338  sspval 8345  lnoval 8376  islno 8377  nmofval 8386  nmoval 8387  nmosetn0 8389  nmolb 8395  0ofval 8408  0oval 8409  0oo 8410  nmlno0lem 8414  blocni 8425  ajfval 8429  isph 8441  phpar 8443  ubthlem1 8489  ubthlem3 8491  ubthlem6 8494  minveclem31 8535  minveclem33 8537  minveceu 8543  hlex 8559  htthlem11 8589  efgh 8668  efghgrpilem 8669  efif 8671  efifo 8679  efif1 8687  shftefif1olem 8696  shftefif1olemOLD 8697  eff1i 8700  effoi 8701  effoiOLD 8702  normvalt 8964  projlem23 9182  projlem31 9190  hsupclt 9280  sshjvalt 9293  sshjval3t 9299  pjspansnt 9475  nmopsetn0 9767  nmfnsetn0 9780  eigvalvalt 9798  nmoplbt 9806  nmfnlbt 9822  adjt 9831  nmlnop0ALT 9893  nmcopexlem1 9924  nmcfnexlem1 9953  branmfnt 10011  hstrlem2 10159  atoml 10280  neifil 10514  eloi 10575  aidm 10599  aidmold 10600  ishoma 10631  ishomb 10632  ismona 10651  isfuna 10664

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 2699  ax-pow 2738  ax-un 2865

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 2500  df-fv 3198

Copyright terms: Public domain