Theorem ovmpo 7549

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447  (class class class)co 7387   ∈ cmpo 7389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  fvproj  8113  seqomlem1  8418  seqomlem4  8421  oav  8475  omv  8476  oev  8478  iunfictbso  10067  fin23lem12  10284  axdc4lem  10408  axcclem  10410  addpipq2  10889  mulpipq2  10892  subval  11412  divval  11839  cnref1o  12944  ixxval  13314  fzval  13470  modval  13833  om2uzrdg  13921  uzrdgsuci  13925  axdc4uzlem  13948  seqval  13977  seqp1  13981  bcval  14269  cnrecnv  15131  risefacval  15974  fallfacval  15975  gcdval  16466  lcmval  16562  imasvscafn  17500  imasvscaval  17501  grpsubval  18917  isghmOLD  19148  lactghmga  19335  efgmval  19642  efgtval  19653  frgpup3lem  19707  dvrval  20312  frlmval  21657  psrvsca  21858  mat1comp  22327  mamulid  22328  mamurid  22329  madufval  22524  xkococnlem  23546  xkococn  23547  cnextval  23948  dscmet  24460  cncfval  24781  htpycom  24875  htpyid  24876  phtpycom  24887  phtpyid  24888  ehl1eudisval  25321  logbval  26676  addsval  27869  subsval  27964  mulsval  28012  divsval  28092  seqsval  28182  om2noseqrdg  28198  noseqrdgsuc  28202  seqsp1  28205  expsval  28311  isismt  28461  clwwlknon  30019  clwwlk0on0  30021  grpodivval  30464  ipval  30632  lnoval  30681  nmoofval  30691  bloval  30710  0ofval  30716  ajfval  30738  hvsubval  30945  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  kbfval  31881  opsqrlem3  32071  dpval  32810  xdivval  32839  smatrcl  33786  smatlem  33787  mdetpmtr12  33815  pstmfval  33886  sxval  34180  ismbfm  34241  dya2iocival  34264  sitgval  34323  sitmval  34340  oddpwdcv  34346  ballotlemgval  34515  vtsval  34628  cvmlift2lem4  35293  icoreval  37341  metf1o  37749  heiborlem3  37807  heiborlem6  37810  heiborlem8  37812  heibor  37815  ldualvs  39130  tendopl  40770  cdlemkuu  40889  dvavsca  41011  dvhvaddval  41084  dvhvscaval  41093  hlhilipval  41943  resubval  42355  redivvald  42430  prjspnval  42604  rrx2xpref1o  48707  fuco22natlem  49334  functhinclem1  49433