HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem oprex 3968
Description: The result of an operation is a set.
Assertion
Ref Expression
oprex |- (AFB) e. V
Proof of Theorem oprex
StepHypRef Expression
1 df-opr 3950 . 2 |- (AFB) = (F` <.A, B>.)
2 fvex 3717 . 2 |- (F` <.A, B>.) e. V
31, 2eqeltr 1536 1 |- (AFB) e. V
Colors of variables: wff set class
Syntax hints:   e. wcel 955  Vcvv 1802  <.cop 2401  ` cfv 3172  (class class class)co 3948
This theorem is referenced by:  oprvalelrn 4024  ndmoprass 4034  ndmoprdistr 4035  ndmord 4036  ndmordi 4037  caopr4 4050  caopr411 4051  caoprdistrr 4053  caoprdilem 4054  caoprlem2 4055  curry1 4082  curry1val 4084  oasuc 4147  omsuc 4149  oesuc 4150  oacl 4154  omcl 4155  oecl 4156  oaordi 4164  oaass 4179  odi 4194  omass 4195  oneo 4196  brecop2 4291  ecopoprtrn 4295  th3qlem1 4298  mapsnen 4410  map1 4411  mapen 4471  mapdom1 4472  mapdom2 4474  mapxpen 4475  xpmapenlem5 4480  mapunen 4482  pwen 4483  unfilem2 4525  unfilem3 4526  aleph1 4843  mapcdaen 4904  cdainf 4909  addcmpblnq 5024  ordpipq 5028  addcompq 5034  addasspq 5035  distrpq 5039  recmulpq 5042  ltsopq 5047  ltapq 5048  ltmpq 5049  1lt2pq 5050  ltaddpq 5051  ltexpq 5052  halfpq 5054  ltbtwnpq 5056  ltrpq 5057  genpprecl 5076  genpn0 5078  genpnnp 5080  genpnmax 5082  genpass 5084  1pr 5089  addclprlem1 5090  addclprlem2 5091  mulclprlem 5093  distrlem1pr 5099  distrlem4pr 5102  distrlem5pr 5103  1idpr 5105  prlem934a 5109  prlem934b 5110  prlem934 5111  ltexprlem4 5117  ltexprlem7 5120  ltapr 5123  prlem936a 5125  prlem936 5127  reclem3pr 5130  reclem4pr 5131  mulcmpblnrlem 5154  mulcmpblnr 5155  ltsrpr 5158  mulcomsr 5170  distrsr 5172  m1m1sr 5174  ltsosr 5175  0lt1sr 5176  1idsr 5179  ltasr 5181  pn0sr 5182  negexsr 5183  recexsrlem 5184  addgt0sr 5185  mulgt0sr 5186  sqgt0sr 5187  recexsr 5188  ssgt0sr 5189  mappsrpr 5190  ltpsrpr 5191  map2psrpr 5192  supsrlem1 5197  supsrlem2 5198  supsrlem3 5199  supsrlem6 5202  axmulcom 5248  axmulass 5250  axdistr 5251  axrnegex 5255  axrrecex 5256  pre-axltadd 5261  pre-axmulgt0 5262  negex 5337  peano2nn 5883  nn1suc 5887  sup2 5998  nnunb 6017  dfuz 6150  uzindOLD 6156  elq 6195  om2uzsuc 6233  seq1lem1 6246  seq1suclem 6253  2shft 6289  shftcan2t 6290  seq1shftid 6293  ioof 6333  icoshftf1oi 6342  uzind4s 6384  fzrevralt 6451  fzshftralt 6454  seq0fval 6467  seqzfval 6469  seqzfn 6471  seq1seqz 6473  seq1seq02t 6475  seq1seq0t 6476  seq1seq0 6477  seq0fn 6478  seqz1 6479  seqzp1 6480  seq00 6482  seq0p1 6483  seqzval2t 6485  dfseq0 6495  cjvalt 6695  facp1t 6873  bcvalt 6895  sumeq2 6923  fsump1slem 6950  fsump1s 6951  fsumadd 6960  csbfsumlem 6964  csbfsum 6965  fsumcom 6966  fsumrev 6967  fsumshft 6969  fsummulc1 6971  fsumconst 6976  fsumcmp 6978  fsumabs 6981  serzsplit 6994  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  binomlem6 7009  bcxmas 7014  climshft 7041  climshft2 7043  iserzshft2 7044  climsub 7066  clim2serzt 7070  iserzext 7071  iserzmulc1 7072  climcmplem 7073  iserzcmp 7078  iserzshft 7080  clim2serz 7081  iserzex 7082  climserzle 7083  caucvg3a 7100  caucvg3lem 7102  caucvg3 7103  iserzabslem 7114  cvgcmp2lem 7116  cvgcmp2 7117  cvgcmp2clem 7118  cvgcmp2c 7119  cvgcmp3ce 7123  isumshft 7139  isumshft2 7140  isum1p 7141  isummulc1 7147  isummulc1ALT 7148  isumsplit 7151  infcvg 7159  fnsmnt 7161  geoser 7169  geolimilem 7170  geolimi 7171  geolim1i 7173  geosum 7176  geoisum 7177  geoisum1 7179  geoisum1c 7180  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  efcltlem1 7246  dfef2 7249  ef0lem 7252  efseq0ex 7253  efclt 7254  efcvg 7256  efcvgfsum 7257  eftval 7258  erelem2 7262  erelem3 7263  erelem6 7266  ege2lem2 7270  ege2le3lem2 7271  efcj 7278  efaddlem5 7284  efaddlem26 7305  efaddlem27 7306  efaddlem28 7307  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  absefm1le 7352  eflegeolem2 7354  sinvalt 7371  cosvalt 7372  sinf 7382  cosf 7383  acdc3 7429  acdc2lem1 7430  acdc2lem2 7431  acdc2 7432  acdc5lem1 7433  acdc5lem2 7434  acdc5 7435  acdc 7437  qnnen 7446  ruclem13 7465  ruclem16 7468  ruclem18 7470  ruclem19 7471  ruclem20 7472  ruclem21 7473  ruclem25 7477  infmap1 7516  infmap2lem2 7522  infmap2 7523  alephadd 7524  alephexp2 7528  cnfval 7696  cnpval 7699  fsumcnlem 7923  grpdivval 8017  grplactval 8033  grplactf1o 8034  sqcn 8270  va1cnlem 8279  sm1cnilem 8281  ipval 8287  ipval2 8291  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem4 8310  ip1cnilem6 8312  nmofval 8357  bloval 8373  ajfval 8400  hmoval 8401  ipasslem6 8426  ipasslem8 8428  ipasslem9 8429  ipblnfi 8447  ubthi 8475  minveclem23 8498  minveclem33 8508  htthlem4 8553  sincolem 8584  shftefif1olem 8661  shftefif1olemOLD 8662  hvsubvalt 8807  hhip 8965  hsn0elch 9041  occllem3 9091  occllem7 9095  shintcl 9208  hosvalt 9433  hosvaltOLD 9434  homvalt 9435  hodvalt 9436  hodvaltOLD 9437  hfsvalt 9438  hfmvalt 9439  hmopex 9719  bravalvalt 9784  kbvalvalt 9794  eigvalt 9800  cnlnadjlem1 9915  kbass2t 9962  kbass5t 9965  strlem2 10088  elgiso 10303  cdrci 10381  hmeogrp 10425  clicls 10466  stoi 10483
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  df-opr 3950
Copyright terms: Public domain