Theorem oprex 4041

Description: The result of an operation is a set.

Assertion

Ref	Expression
oprex	|- (AFB) e. V

Proof of Theorem oprex

Step	Hyp	Ref	Expression
1		df-opr 4023	. 2 |- (AFB) = (F` <.A, B>.)
2		fvex 3843	. 2 |- (F` <.A, B>.) e. V
3	1, 2	eqeltri 1587	1 |- (AFB) e. V

Syntax hints:   e. wcel 994  Vcvv 1857  <.cop 2469  ` cfv 3263  (class class class)co 4021

This theorem is referenced by:  oprvelrn 4100  ndmoprass 4109  ndmoprdistr 4110  ndmord 4111  ndmordi 4112  caopr4 4125  caopr411 4126  caoprdistrr 4128  caoprdilem 4129  caoprlem2 4130  curry1 4193  curry1val 4195  curry2 4196  curry2val 4198  onopruni 4210  onopriun 4211  oasuc 4299  omsuc 4301  oesuc 4302  oacl 4306  omcl 4307  oecl 4308  oaordi 4316  oaass 4331  odi 4346  omass 4347  oneo 4348  brecop2 4448  ecopoprtrn 4452  th3qlem1 4455  mapsnen 4570  map1 4571  mapen 4638  mapdom1 4639  mapdom2 4641  mapxpen 4642  xpmapenlem5 4647  mapunen 4649  pwen 4650  unfilem2 4695  unfilem3 4696  aleph1 5021  mapcdaen 5084  cdainf 5089  nnacda 5090  nnaun 5091  addcmpblnq 5206  ordpipq 5210  addcompq 5216  addasspq 5217  distrpq 5221  recmulpq 5224  ltsopq 5229  ltapq 5230  ltmpq 5231  1lt2pq 5232  ltaddpq 5233  ltexpq 5234  halfpq 5236  ltbtwnpq 5238  ltrpq 5239  genpprecl 5258  genpn0 5260  genpnnp 5262  genpnmax 5264  genpass 5266  1pr 5271  addclprlem1 5272  addclprlem2 5273  mulclprlem 5275  distrlem1pr 5281  distrlem4pr 5284  distrlem5pr 5285  1idpr 5287  prlem934a 5291  prlem934b 5292  prlem934 5293  ltexprlem4 5299  ltexprlem7 5302  ltapr 5305  prlem936a 5307  prlem936 5309  reclem3pr 5312  reclem4pr 5313  mulcmpblnrlem 5336  mulcmpblnr 5337  ltsrpr 5340  mulcomsr 5352  distrsr 5354  m1m1sr 5356  ltsosr 5357  0lt1sr 5358  1idsr 5361  ltasr 5363  pn0sr 5364  negexsr 5365  recexsrlem 5366  addgt0sr 5367  mulgt0sr 5368  sqgt0sr 5369  recexsr 5370  ssgt0sr 5371  mappsrpr 5372  ltpsrpr 5373  map2psrpr 5374  supsrlem1 5379  supsrlem2 5380  supsrlem3 5381  supsrlem6 5384  axmulcom 5430  axmulass 5432  axdistr 5433  axrnegex 5437  axrrecex 5438  pre-axltadd 5443  pre-axmulgt0 5444  negex 5519  peano2nn 6080  nn1suc 6084  sup2 6219  nnunb 6238  dfuzi 6373  uzindOLD 6379  elq 6396  modval 6460  ioof 6527  icoshftf1oii 6536  uzind4s 6579  fzen 6622  fzrevral 6650  fzshftral 6653  om2uzsuci 6659  cardfz 6671  seq1lem1 6674  seq1suclem 6681  2shfti 6717  shftcan2 6718  seq1shftid 6721  seq0fval 6730  seqzfval 6732  seqzfn 6734  seq1seqz 6736  seq1seq02 6738  seq1seq01 6739  seq1seq0 6740  seq0fn 6741  seqz1 6742  seqzp1 6743  seq00 6745  seq0p1 6746  seqzval2 6748  dfseq0 6758  cjval 6964  facp1 7139  bcval 7161  sumeq2 7188  fsump1slem 7215  fsump1s 7216  fsumadd 7225  csbfsumlem 7229  csbfsum 7230  fsumcom 7231  fsumrev 7232  fsumshft 7234  fsummulc1 7236  fsumconst 7241  fsumcmp 7243  fsumabs 7246  serzsplit 7259  binomlem2 7270  binomlem3 7271  binomlem4 7272  binomlem5 7273  binomlem6 7274  bcxmas 7279  climshfti 7307  climshft2i 7309  iserzshft2i 7310  climsub 7333  clim2serz 7337  iserzex 7338  iserzmulc1 7339  climcmplem 7340  iserzcmp 7345  iserzshfti 7347  clim2serzi 7348  iserzexi 7349  climserzlei 7350  caucvg3ai 7367  caucvg3lem 7369  caucvg3i 7370  iserzabslem 7381  cvgcmp2lem 7383  cvgcmp2i 7384  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  cvgcmp2ci 7387  cvgcmp3cei 7391  isumshfti 7408  isumshft2i 7409  isum1p 7410  isummulc1 7416  isummulc1iALT 7417  isumspliti 7420  infcvgi 7428  arisumi 7430  explecnv 7438  geoseri 7439  geolimilem 7440  geolimi 7441  geolim1i 7443  geosumi 7446  geoisum 7447  geoisum1 7449  geoisum1c 7450  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag 7463  fsum0diag2 7464  fsum0diag4 7466  efcltlem1 7509  dfef2i 7512  ef0lem 7515  efseq0ex 7516  efcl 7517  efcvg 7519  efcvgfsum 7520  eftval 7521  erelem2 7525  erelem3 7526  erelem6 7529  ege2lem2 7533  ege2le3lem2 7534  efcji 7541  efaddlem5 7547  efaddlem26 7568  efaddlem27 7569  efaddlem28 7570  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  absefm1lei 7620  eflegeolem2 7622  sinval 7637  cosval 7638  sinf 7648  cosf 7649  acdc3 7698  acdc2lem1 7700  acdc2lem2 7701  acdc2 7702  acdc5lem1 7703  acdc5lem2 7704  acdc5 7705  acdc 7707  qnnen 7715  ruclem13 7734  ruclem16 7737  ruclem18 7739  ruclem19 7740  ruclem20 7741  ruclem21 7742  ruclem25 7746  infmap1 7785  infmap2lem2 7792  infmap2 7793  alephadd 7794  alephexp2 7798  cnfval 7966  cnpval 7969  fsumcnlem 8200  grpdivval 8300  grplactval 8338  grplactf1o 8339  sqcn 8589  va1cnlem 8599  sm1cnilem 8601  ipval 8607  ipval2 8611  ip1cnilem2 8628  ip1cnilem3 8629  ip1cnilem4 8630  ip1cnilem6 8632  nmofval 8679  bloval 8696  ajfval 8724  hmoval 8725  ipasslem6 8751  ipasslem8 8753  ipasslem9 8754  ipblnfi 8772  ubthi 8804  minveclem23 8827  minveclem33 8837  htthlem4 8885  sincolem 8932  shftefif1olem 9013  hvsubval 9161  hhip 9320  hsn0elch 9396  occllem3 9451  occllem7 9455  shintcli 9569  hosval 9792  hosvalOLD 9793  homval 9794  hodval 9795  hodvalOLD 9796  hfsval 9797  hfmval 9798  hmopex 10082  bravalval 10148  kbvalval 10158  eigval1 10164  cnlnadjlem1 10279  kbass2 10330  kbass5 10333  strlem2 10459  elgiso 10683  nfwval 10874  expm 10937  cdrci 10994  hmeogrp 11044  clicls 11138  stoi 11145  idsubfun 11312  subtopmet 11506  reconnlem1 11507  filmapf 11688  flimff 11707  gaid 11776  gapm 11784  sdclem2 11876  sdc 11877  fsum00 11883  fsumltisumi 11886  fsumlt1 11894  metf1o 11907  metsstop 11909  mettrifi2 11913  geomcau 11914  lmclim2 11915  metdcn 11918  icoopnst 11940  iocopnst 11941  addccncf 11945  sub1cncf 11946  sub2cncf 11947  sstotbnd 11992  totbndss 11993  totbndbnd 12000  heiborlem1 12011  heiborlem28 12038  heiborlem29 12039  bfplem8 12061  rrnval 12069  rrndm 12071  rrnmet 12072  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  ismrer1 12080  phtpyfval 12088  phtpyval 12089  phtpycom 12092  phtpycolem1 12093  phtpycolem2 12094  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097  phtpcval 12100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-uni 2570  df-fv 3279  df-opr 4023

Copyright terms: Public domain