Theorem ovmpo 7528

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

Step	Hyp	Ref	Expression
1		ovmpo.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpog.1	. . 3 ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
3		ovmpog.2	. . 3 ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
4		ovmpog.3	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
5	2, 3, 4	ovmpog 7527	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
6	1, 5	mp3an3 1453	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  (class class class)co 7368   ∈ cmpo 7370

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  fvproj  8086  seqomlem1  8391  seqomlem4  8394  oav  8448  omv  8449  oev  8451  iunfictbso  10036  fin23lem12  10253  axdc4lem  10377  axcclem  10379  addpipq2  10859  mulpipq2  10862  subval  11383  divval  11810  cnref1o  12910  ixxval  13281  fzval  13437  modval  13803  om2uzrdg  13891  uzrdgsuci  13895  axdc4uzlem  13918  seqval  13947  seqp1  13951  bcval  14239  cnrecnv  15100  risefacval  15943  fallfacval  15944  gcdval  16435  lcmval  16531  imasvscafn  17470  imasvscaval  17471  grpsubval  18927  isghmOLD  19157  lactghmga  19346  efgmval  19653  efgtval  19664  frgpup3lem  19718  dvrval  20351  frlmval  21715  psrvsca  21917  mat1comp  22396  mamulid  22397  mamurid  22398  madufval  22593  xkococnlem  23615  xkococn  23616  cnextval  24017  dscmet  24528  cncfval  24849  htpycom  24943  htpyid  24944  phtpycom  24955  phtpyid  24956  ehl1eudisval  25389  logbval  26744  addsval  27970  subsval  28068  mulsval  28117  divsval  28197  seqsval  28296  om2noseqrdg  28312  noseqrdgsuc  28316  seqsp1  28319  expsval  28433  isismt  28618  clwwlknon  30177  clwwlk0on0  30179  grpodivval  30623  ipval  30791  lnoval  30840  nmoofval  30850  bloval  30869  0ofval  30875  ajfval  30897  hvsubval  31104  hosmval  31823  hommval  31824  hodmval  31825  hfsmval  31826  hfmmval  31827  kbfval  32040  opsqrlem3  32230  dpval  32982  xdivval  33011  smatrcl  33974  smatlem  33975  mdetpmtr12  34003  pstmfval  34074  sxval  34368  ismbfm  34429  dya2iocival  34451  sitgval  34510  sitmval  34527  oddpwdcv  34533  ballotlemgval  34702  vtsval  34815  cvmlift2lem4  35522  icoreval  37608  metf1o  38006  heiborlem3  38064  heiborlem6  38067  heiborlem8  38069  heibor  38072  ldualvs  39513  tendopl  41152  cdlemkuu  41271  dvavsca  41393  dvhvaddval  41466  dvhvscaval  41475  hlhilipval  42325  resubval  42737  redivvald  42812  prjspnval  42974  rrx2xpref1o  49078  fuco22natlem  49704  functhinclem1  49803