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

Theorem ovmpo 7387
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 7386 . 2 ((𝐴𝐶𝐵𝐷𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
61, 5mp3an3 1452 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2111  Vcvv 3420  (class class class)co 7231  cmpo 7233
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-sbc 3709  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-id 5469  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-iota 6355  df-fun 6399  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236
This theorem is referenced by:  fvproj  7921  seqomlem1  8206  seqomlem4  8209  oav  8258  omv  8259  oev  8261  iunfictbso  9752  fin23lem12  9969  axdc4lem  10093  axcclem  10095  addpipq2  10574  mulpipq2  10577  subval  11093  divval  11516  cnref1o  12605  ixxval  12967  fzval  13121  modval  13468  om2uzrdg  13553  uzrdgsuci  13557  axdc4uzlem  13580  seqval  13609  seqp1  13613  bcval  13894  cnrecnv  14752  risefacval  15594  fallfacval  15595  gcdval  16079  lcmval  16173  imasvscafn  17066  imasvscaval  17067  grpsubval  18437  isghm  18646  lactghmga  18821  efgmval  19126  efgtval  19137  frgpup3lem  19191  dvrval  19727  frlmval  20734  psrvsca  20940  mat1comp  21361  mamulid  21362  mamurid  21363  madufval  21558  xkococnlem  22580  xkococn  22581  cnextval  22982  dscmet  23494  cncfval  23809  htpycom  23897  htpyid  23898  phtpycom  23909  phtpyid  23910  ehl1eudisval  24342  logbval  25673  isismt  26649  clwwlknon  28197  clwwlk0on0  28199  grpodivval  28640  ipval  28808  lnoval  28857  nmoofval  28867  bloval  28886  0ofval  28892  ajfval  28914  hvsubval  29121  hosmval  29840  hommval  29841  hodmval  29842  hfsmval  29843  hfmmval  29844  kbfval  30057  opsqrlem3  30247  dpval  30908  xdivval  30937  smatrcl  31484  smatlem  31485  mdetpmtr12  31513  pstmfval  31584  sxval  31894  ismbfm  31955  dya2iocival  31976  sitgval  32035  sitmval  32052  oddpwdcv  32058  ballotlemgval  32226  vtsval  32353  cvmlift2lem4  33004  addsval  33889  icoreval  35287  metf1o  35676  heiborlem3  35734  heiborlem6  35737  heiborlem8  35739  heibor  35742  ldualvs  36914  tendopl  38553  cdlemkuu  38672  dvavsca  38794  dvhvaddval  38867  dvhvscaval  38876  hlhilipval  39726  resubval  40086  prjspnval  40191  rrx2xpref1o  45765  functhinclem1  46023
  Copyright terms: Public domain W3C validator