Theorem oprex 3974

Description: The result of an operation is a set.

Assertion

Ref	Expression
oprex	⊢ (AFB) ∈ V

Proof of Theorem oprex

Step	Hyp	Ref	Expression
1		df-opr 3956	. 2 ⊢ (AFB) = (F ‘⟨A, B⟩)
2		fvex 3723	. 2 ⊢ (F ‘⟨A, B⟩) ∈ V
3	1, 2	eqeltr 1541	1 ⊢ (AFB) ∈ V

Syntax hints:   ∈ wcel 956  Vcvv 1807  ⟨cop 2407   ‘cfv 3177  (class class class)co 3954

This theorem is referenced by:  oprvalelrn 4030  ndmoprass 4040  ndmoprdistr 4041  ndmord 4042  ndmordi 4043  caopr4 4056  caopr411 4057  caoprdistrr 4059  caoprdilem 4060  caoprlem2 4061  curry1 4088  curry1val 4090  oasuc 4153  omsuc 4155  oesuc 4156  oacl 4160  omcl 4161  oecl 4162  oaordi 4170  oaass 4185  odi 4200  omass 4201  oneo 4202  brecop2 4297  ecopoprtrn 4301  th3qlem1 4304  mapsnen 4416  map1 4417  mapen 4477  mapdom1 4478  mapdom2 4480  mapxpen 4481  xpmapenlem5 4486  mapunen 4488  pwen 4489  unfilem2 4531  unfilem3 4532  aleph1 4851  mapcdaen 4912  cdainf 4917  addcmpblnq 5032  ordpipq 5036  addcompq 5042  addasspq 5043  distrpq 5047  recmulpq 5050  ltsopq 5055  ltapq 5056  ltmpq 5057  1lt2pq 5058  ltaddpq 5059  ltexpq 5060  halfpq 5062  ltbtwnpq 5064  ltrpq 5065  genpprecl 5084  genpn0 5086  genpnnp 5088  genpnmax 5090  genpass 5092  1pr 5097  addclprlem1 5098  addclprlem2 5099  mulclprlem 5101  distrlem1pr 5107  distrlem4pr 5110  distrlem5pr 5111  1idpr 5113  prlem934a 5117  prlem934b 5118  prlem934 5119  ltexprlem4 5125  ltexprlem7 5128  ltapr 5131  prlem936a 5133  prlem936 5135  reclem3pr 5138  reclem4pr 5139  mulcmpblnrlem 5162  mulcmpblnr 5163  ltsrpr 5166  mulcomsr 5178  distrsr 5180  m1m1sr 5182  ltsosr 5183  0lt1sr 5184  1idsr 5187  ltasr 5189  pn0sr 5190  negexsr 5191  recexsrlem 5192  addgt0sr 5193  mulgt0sr 5194  sqgt0sr 5195  recexsr 5196  ssgt0sr 5197  mappsrpr 5198  ltpsrpr 5199  map2psrpr 5200  supsrlem1 5205  supsrlem2 5206  supsrlem3 5207  supsrlem6 5210  axmulcom 5256  axmulass 5258  axdistr 5259  axrnegex 5263  axrrecex 5264  pre-axltadd 5269  pre-axmulgt0 5270  negex 5345  peano2nn 5891  nn1suc 5895  sup2 6006  nnunb 6025  dfuz 6158  uzindOLD 6164  elq 6203  om2uzsuc 6241  seq1lem1 6254  seq1suclem 6261  2shft 6297  shftcan2t 6298  seq1shftid 6301  ioof 6341  icoshftf1oi 6350  uzind4s 6392  fzrevralt 6459  fzshftralt 6462  seq0fval 6475  seqzfval 6477  seqzfn 6479  seq1seqz 6481  seq1seq02t 6483  seq1seq0t 6484  seq1seq0 6485  seq0fn 6486  seqz1 6487  seqzp1 6488  seq00 6490  seq0p1 6491  seqzval2t 6493  dfseq0 6503  cjvalt 6703  facp1t 6881  bcvalt 6903  sumeq2 6931  fsump1slem 6958  fsump1s 6959  fsumadd 6968  csbfsumlem 6972  csbfsum 6973  fsumcom 6974  fsumrev 6975  fsumshft 6977  fsummulc1 6979  fsumconst 6984  fsumcmp 6986  fsumabs 6989  serzsplit 7002  binomlem2 7013  binomlem3 7014  binomlem4 7015  binomlem5 7016  binomlem6 7017  bcxmas 7022  climshft 7049  climshft2 7051  iserzshft2 7052  climsub 7074  clim2serzt 7078  iserzext 7079  iserzmulc1 7080  climcmplem 7081  iserzcmp 7086  iserzshft 7088  clim2serz 7089  iserzex 7090  climserzle 7091  caucvg3a 7108  caucvg3lem 7110  caucvg3 7111  iserzabslem 7122  cvgcmp2lem 7124  cvgcmp2 7125  cvgcmp2clem 7126  cvgcmp2c 7127  cvgcmp3ce 7131  isumshft 7147  isumshft2 7148  isum1p 7149  isummulc1 7155  isummulc1ALT 7156  isumsplit 7159  infcvg 7167  fnsmnt 7169  geoser 7177  geolimilem 7178  geolimi 7179  geolim1i 7181  geosum 7184  geoisum 7185  geoisum1 7187  geoisum1c 7188  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202  fsum0diag4 7204  efcltlem1 7254  dfef2 7257  ef0lem 7260  efseq0ex 7261  efclt 7262  efcvg 7264  efcvgfsum 7265  eftval 7266  erelem2 7270  erelem3 7271  erelem6 7274  ege2lem2 7278  ege2le3lem2 7279  efcj 7286  efaddlem5 7292  efaddlem26 7313  efaddlem27 7314  efaddlem28 7315  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  absefm1le 7360  eflegeolem2 7362  sinvalt 7379  cosvalt 7380  sinf 7390  cosf 7391  acdc3 7437  acdc2lem1 7438  acdc2lem2 7439  acdc2 7440  acdc5lem1 7441  acdc5lem2 7442  acdc5 7443  acdc 7445  qnnen 7454  ruclem13 7473  ruclem16 7476  ruclem18 7478  ruclem19 7479  ruclem20 7480  ruclem21 7481  ruclem25 7485  infmap1 7524  infmap2lem2 7530  infmap2 7531  alephadd 7532  alephexp2 7536  cnfval 7706  cnpval 7709  fsumcnlem 7939  grpdivval 8032  grplactval 8048  grplactf1o 8049  sqcn 8283  va1cnlem 8292  sm1cnilem 8294  ipval 8300  ipval2 8304  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem4 8323  ip1cnilem6 8325  nmofval 8370  bloval 8386  ajfval 8413  hmoval 8414  ipasslem6 8439  ipasslem8 8441  ipasslem9 8442  ipblnfi 8460  ubthi 8488  minveclem23 8511  minveclem33 8521  htthlem4 8566  sincolem 8603  shftefif1olem 8680  hvsubvalt 8825  hhip 8983  hsn0elch 9059  occllem3 9114  occllem7 9118  shintcl 9231  hosvalt 9456  hosvaltOLD 9457  homvalt 9458  hodvalt 9459  hodvaltOLD 9460  hfsvalt 9461  hfmvalt 9462  hmopex 9742  bravalvalt 9807  kbvalvalt 9817  eigvalt 9823  cnlnadjlem1 9938  kbass2t 9988  kbass5t 9991  strlem2 10116  elgiso 10332  cdrci 10417  hmeogrp 10461  clicls 10502  stoi 10519

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  df-opr 3956

Copyright terms: Public domain