Theorem ovmpo 7521

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 7520	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
6	1, 5	mp3an3 1453	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  (class class class)co 7361   ∈ cmpo 7363

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 5232  ax-pr 5371

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366

This theorem is referenced by:  fvproj  8078  seqomlem1  8383  seqomlem4  8386  oav  8440  omv  8441  oev  8443  iunfictbso  10030  fin23lem12  10247  axdc4lem  10371  axcclem  10373  addpipq2  10853  mulpipq2  10856  subval  11378  divval  11805  cnref1o  12929  ixxval  13300  fzval  13457  modval  13824  om2uzrdg  13912  uzrdgsuci  13916  axdc4uzlem  13939  seqval  13968  seqp1  13972  bcval  14260  cnrecnv  15121  risefacval  15967  fallfacval  15968  gcdval  16459  lcmval  16555  imasvscafn  17495  imasvscaval  17496  grpsubval  18955  isghmOLD  19185  lactghmga  19374  efgmval  19681  efgtval  19692  frgpup3lem  19746  dvrval  20377  frlmval  21741  psrvsca  21941  mat1comp  22418  mamulid  22419  mamurid  22420  madufval  22615  xkococnlem  23637  xkococn  23638  cnextval  24039  dscmet  24550  cncfval  24868  htpycom  24956  htpyid  24957  phtpycom  24968  phtpyid  24969  ehl1eudisval  25401  logbval  26746  addsval  27971  subsval  28069  mulsval  28118  divsval  28198  seqsval  28297  om2noseqrdg  28313  noseqrdgsuc  28317  seqsp1  28320  expsval  28434  isismt  28619  clwwlknon  30178  clwwlk0on0  30180  grpodivval  30624  ipval  30792  lnoval  30841  nmoofval  30851  bloval  30870  0ofval  30876  ajfval  30898  hvsubval  31105  hosmval  31824  hommval  31825  hodmval  31826  hfsmval  31827  hfmmval  31828  kbfval  32041  opsqrlem3  32231  dpval  32967  xdivval  32996  smatrcl  33959  smatlem  33960  mdetpmtr12  33988  pstmfval  34059  sxval  34353  ismbfm  34414  dya2iocival  34436  sitgval  34495  sitmval  34512  oddpwdcv  34518  ballotlemgval  34687  vtsval  34800  cvmlift2lem4  35507  icoreval  37686  metf1o  38093  heiborlem3  38151  heiborlem6  38154  heiborlem8  38156  heibor  38159  ldualvs  39600  tendopl  41239  cdlemkuu  41358  dvavsca  41480  dvhvaddval  41553  dvhvscaval  41562  hlhilipval  42412  resubval  42816  redivvald  42891  prjspnval  43066  rrx2xpref1o  49209  fuco22natlem  49835  functhinclem1  49934