Theorem ovmpo 7527

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429  (class class class)co 7367   ∈ cmpo 7369

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 2708  ax-sep 5231  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  fvproj  8084  seqomlem1  8389  seqomlem4  8392  oav  8446  omv  8447  oev  8449  iunfictbso  10036  fin23lem12  10253  axdc4lem  10377  axcclem  10379  addpipq2  10859  mulpipq2  10862  subval  11384  divval  11811  cnref1o  12935  ixxval  13306  fzval  13463  modval  13830  om2uzrdg  13918  uzrdgsuci  13922  axdc4uzlem  13945  seqval  13974  seqp1  13978  bcval  14266  cnrecnv  15127  risefacval  15973  fallfacval  15974  gcdval  16465  lcmval  16561  imasvscafn  17501  imasvscaval  17502  grpsubval  18961  isghmOLD  19191  lactghmga  19380  efgmval  19687  efgtval  19698  frgpup3lem  19752  dvrval  20383  frlmval  21728  psrvsca  21928  mat1comp  22405  mamulid  22406  mamurid  22407  madufval  22602  xkococnlem  23624  xkococn  23625  cnextval  24026  dscmet  24537  cncfval  24855  htpycom  24943  htpyid  24944  phtpycom  24955  phtpyid  24956  ehl1eudisval  25388  logbval  26730  addsval  27954  subsval  28052  mulsval  28101  divsval  28181  seqsval  28280  om2noseqrdg  28296  noseqrdgsuc  28300  seqsp1  28303  expsval  28417  isismt  28602  clwwlknon  30160  clwwlk0on0  30162  grpodivval  30606  ipval  30774  lnoval  30823  nmoofval  30833  bloval  30852  0ofval  30858  ajfval  30880  hvsubval  31087  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  kbfval  32023  opsqrlem3  32213  dpval  32949  xdivval  32978  smatrcl  33940  smatlem  33941  mdetpmtr12  33969  pstmfval  34040  sxval  34334  ismbfm  34395  dya2iocival  34417  sitgval  34476  sitmval  34493  oddpwdcv  34499  ballotlemgval  34668  vtsval  34781  cvmlift2lem4  35488  icoreval  37669  metf1o  38076  heiborlem3  38134  heiborlem6  38137  heiborlem8  38139  heibor  38142  ldualvs  39583  tendopl  41222  cdlemkuu  41341  dvavsca  41463  dvhvaddval  41536  dvhvscaval  41545  hlhilipval  42395  resubval  42799  redivvald  42874  prjspnval  43049  rrx2xpref1o  49194  fuco22natlem  49820  functhinclem1  49919