Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpo Structured version   Visualization version   GIF version

Theorem ovmpo 7294
 Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
Hypotheses
Ref Expression
ovmpog.1 (𝑥 = 𝐴𝑅 = 𝐺)
ovmpog.2 (𝑦 = 𝐵𝐺 = 𝑆)
ovmpog.3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
ovmpo.4 𝑆 ∈ V
Assertion
Ref Expression
ovmpo ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem ovmpo
StepHypRef Expression
1 ovmpo.4 . 2 𝑆 ∈ V
2 ovmpog.1 . . 3 (𝑥 = 𝐴𝑅 = 𝐺)
3 ovmpog.2 . . 3 (𝑦 = 𝐵𝐺 = 𝑆)
4 ovmpog.3 . . 3 𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)
52, 3, 4ovmpog 7293 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
61, 5mp3an3 1447 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2114  Vcvv 3469  (class class class)co 7140   ∈ cmpo 7142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-iota 6293  df-fun 6336  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145 This theorem is referenced by:  fvproj  7815  seqomlem1  8073  seqomlem4  8076  oav  8123  omv  8124  oev  8126  iunfictbso  9529  fin23lem12  9742  axdc4lem  9866  axcclem  9868  addpipq2  10347  mulpipq2  10350  subval  10866  divval  11289  cnref1o  12372  ixxval  12734  fzval  12887  modval  13234  om2uzrdg  13319  uzrdgsuci  13323  axdc4uzlem  13346  seqval  13375  seqp1  13379  bcval  13660  cnrecnv  14515  risefacval  15353  fallfacval  15354  gcdval  15834  lcmval  15925  imasvscafn  16801  imasvscaval  16802  grpsubval  18140  isghm  18349  lactghmga  18524  efgmval  18829  efgtval  18840  frgpup3lem  18894  dvrval  19429  frlmval  20435  psrvsca  20627  mat1comp  21043  mamulid  21044  mamurid  21045  madufval  21240  xkococnlem  22262  xkococn  22263  cnextval  22664  dscmet  23177  cncfval  23491  htpycom  23579  htpyid  23580  phtpycom  23591  phtpyid  23592  ehl1eudisval  24023  logbval  25350  isismt  26326  clwwlknon  27873  clwwlk0on0  27875  grpodivval  28316  ipval  28484  lnoval  28533  nmoofval  28543  bloval  28562  0ofval  28568  ajfval  28590  hvsubval  28797  hosmval  29516  hommval  29517  hodmval  29518  hfsmval  29519  hfmmval  29520  kbfval  29733  opsqrlem3  29923  dpval  30576  xdivval  30605  smatrcl  31118  smatlem  31119  mdetpmtr12  31147  pstmfval  31213  sxval  31523  ismbfm  31584  dya2iocival  31605  sitgval  31664  sitmval  31681  oddpwdcv  31687  ballotlemgval  31855  vtsval  31982  cvmlift2lem4  32627  icoreval  34731  metf1o  35152  heiborlem3  35210  heiborlem6  35213  heiborlem8  35215  heibor  35218  ldualvs  36392  tendopl  38031  cdlemkuu  38150  dvavsca  38272  dvhvaddval  38345  dvhvscaval  38354  hlhilipval  39204  resubval  39450  prjspnval  39541  rrx2xpref1o  45072
 Copyright terms: Public domain W3C validator