Theorem oprex 3922

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 3904	. 2 |- (AFB) = (F` <.A, B>.)
2		fvex 3671	. 2 |- (F` <.A, B>.) e. V
3	1, 2	eqeltr 1520	1 |- (AFB) e. V

Syntax hints:   e. wcel 1105  Vcvv 1786  <.cop 2382  ` cfv 3145  (class class class)co 3902

This theorem is referenced by:  oprvalelrn 3978  ndmoprass 3988  ndmoprdistr 3989  ndmord 3990  ndmordi 3991  caopr4 4004  caopr411 4005  caoprdistrr 4007  caoprdilem 4008  caoprlem2 4009  curry1 4036  curry1val 4038  oasuc 4101  omsuc 4103  oesuc 4104  oacl 4108  omcl 4109  oecl 4110  oaordi 4118  oaass 4133  odi 4148  omass 4149  oneo 4150  brecop2 4245  ecopoprtrn 4249  th3qlem1 4252  mapsnen 4364  map1 4365  mapen 4423  mapdom1 4424  mapdom2 4426  mapxpen 4427  xpmapenlem5 4432  mapunen 4434  pwen 4435  unfilem2 4477  unfilem3 4478  aleph1 4794  mapcdaen 4855  cdainf 4860  addcmpblnq 4975  ordpipq 4979  addcompq 4985  addasspq 4986  distrpq 4990  recmulpq 4993  ltsopq 4998  ltapq 4999  ltmpq 5000  1lt2pq 5001  ltaddpq 5002  ltexpq 5003  halfpq 5005  ltbtwnpq 5007  ltrpq 5008  genpprecl 5027  genpn0 5029  genpnnp 5031  genpnmax 5033  genpass 5035  1pr 5040  addclprlem1 5041  addclprlem2 5042  mulclprlem 5044  distrlem1pr 5050  distrlem4pr 5053  distrlem5pr 5054  1idpr 5056  prlem934a 5060  prlem934b 5061  prlem934 5062  ltexprlem4 5068  ltexprlem7 5071  ltapr 5074  prlem936a 5076  prlem936 5078  reclem3pr 5081  reclem4pr 5082  mulcmpblnrlem 5105  mulcmpblnr 5106  ltsrpr 5109  mulcomsr 5121  distrsr 5123  m1m1sr 5125  ltsosr 5126  0lt1sr 5127  1idsr 5130  ltasr 5132  pn0sr 5133  negexsr 5134  recexsrlem 5135  addgt0sr 5136  mulgt0sr 5137  sqgt0sr 5138  recexsr 5139  ssgt0sr 5140  mappsrpr 5141  ltpsrpr 5142  map2psrpr 5143  supsrlem1 5148  supsrlem2 5149  supsrlem3 5150  supsrlem6 5153  axmulcom 5199  axmulass 5201  axdistr 5202  axrnegex 5206  axrrecex 5207  pre-axltadd 5212  pre-axmulgt0 5213  negex 5288  peano2nn 5834  nn1suc 5838  sup2 5949  nnunb 5968  dfuz 6101  uzindOLD 6107  elq 6146  om2uzsuc 6184  seq1lem1 6197  seq1suclem 6204  2shft 6240  shftcan2t 6241  seq1shftid 6244  ioof 6284  icoshftf1oi 6293  uzind4s 6335  fzrevralt 6402  fzshftralt 6405  seq0fval 6418  seqzfval 6420  seqzfn 6422  seq1seqz 6424  seq1seq02t 6426  seq1seq0t 6427  seq1seq0 6428  seq0fn 6429  seqz1 6430  seqzp1 6431  seq00 6433  seq0p1 6434  seqzval2t 6436  dfseq0 6446  cjvalt 6646  facp1t 6824  bcvalt 6846  sumeq2 6874  fsump1slem 6901  fsump1s 6902  fsumadd 6911  csbfsumlem 6915  csbfsum 6916  fsumcom 6917  fsumrev 6918  fsumshft 6920  fsummulc1 6922  fsumconst 6927  fsumcmp 6929  fsumabs 6932  serzsplit 6945  binomlem2 6956  binomlem3 6957  binomlem4 6958  binomlem5 6959  binomlem6 6960  bcxmas 6965  climshft 6992  climshft2 6994  iserzshft2 6995  climsub 7017  clim2serzt 7021  iserzext 7022  iserzmulc1 7023  climcmplem 7024  iserzcmp 7029  iserzshft 7031  clim2serz 7032  iserzex 7033  climserzle 7034  caucvg3a 7051  caucvg3lem 7053  caucvg3 7054  iserzabslem 7065  cvgcmp2lem 7067  cvgcmp2 7068  cvgcmp2clem 7069  cvgcmp2c 7070  cvgcmp3ce 7074  isumshft 7090  isumshft2 7091  isum1p 7092  isummulc1 7098  isummulc1ALT 7099  isumsplit 7102  infcvg 7110  fnsmnt 7112  geoser 7120  geolimilem 7121  geolimi 7122  geolim1i 7124  geosum 7127  geoisum 7128  geoisum1 7130  geoisum1c 7131  cvgratlem5 7140  fsum0diaglem2 7143  fsum0diag 7144  fsum0diag2 7145  fsum0diag4 7147  efcltlem1 7197  dfef2 7200  ef0lem 7203  efseq0ex 7204  efclt 7205  efcvg 7207  efcvgfsum 7208  eftval 7209  erelem2 7213  erelem3 7214  erelem6 7217  ege2lem2 7221  ege2le3lem2 7222  efcj 7229  efaddlem5 7235  efaddlem26 7256  efaddlem27 7257  efaddlem28 7258  ef1tllem 7274  ef01tllem1 7276  ef01tllem2 7277  absefm1le 7303  eflegeolem2 7305  sinvalt 7322  cosvalt 7323  sinf 7333  cosf 7334  acdc3 7380  acdc2lem1 7381  acdc2lem2 7382  acdc2 7383  acdc5lem1 7384  acdc5lem2 7385  acdc5 7386  acdc 7388  qnnen 7397  ruclem13 7416  ruclem16 7419  ruclem18 7421  ruclem19 7422  ruclem20 7423  ruclem21 7424  ruclem25 7428  infmap1 7467  infmap2lem2 7473  infmap2 7474  alephadd 7475  alephexp2 7479  cnfval 7644  cnpval 7647  fsumcnlem 7871  grpdivval 7965  grplactval 7981  grplactf1o 7982  sqcn 8207  va1cnlem 8214  sm1cnilem 8216  ipval 8222  ipval2 8226  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem4 8245  ip1cnilem6 8247  nmofval 8292  bloval 8308  ajfval 8335  hmoval 8336  ipasslem6 8361  ipasslem8 8363  ipasslem9 8364  ipblnfi 8382  ubthi 8410  minveclem23 8433  minveclem33 8443  htthlem4 8487  sincolem 8497  shftefif1olem 8574  shftefif1olemOLD 8575  elgiso 8665  cdrci 8738  hmeogrp 8776  clicls 8816  stoi 8833  hvsubvalt 9035  hhip 9193  hsn0elch 9271  occllem3 9305  occllem7 9309  shintcl 9422  hosvalt 9647  hosvaltOLD 9648  homvalt 9649  hodvalt 9650  hodvaltOLD 9651  hfsvalt 9652  hfmvalt 9653  hmopex 9933  bravalvalt 9998  kbvalvalt 10008  eigvalt 10014  cnlnadjlem1 10129  kbass2t 10176  kbass5t 10179  strlem2 10302

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-uni 2472  df-fv 3161  df-opr 3904

Copyright terms: Public domain