Theorem ovmpo 7529

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444  (class class class)co 7369   ∈ cmpo 7371

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  fvproj  8090  seqomlem1  8395  seqomlem4  8398  oav  8452  omv  8453  oev  8455  iunfictbso  10043  fin23lem12  10260  axdc4lem  10384  axcclem  10386  addpipq2  10865  mulpipq2  10868  subval  11388  divval  11815  cnref1o  12920  ixxval  13290  fzval  13446  modval  13809  om2uzrdg  13897  uzrdgsuci  13901  axdc4uzlem  13924  seqval  13953  seqp1  13957  bcval  14245  cnrecnv  15107  risefacval  15950  fallfacval  15951  gcdval  16442  lcmval  16538  imasvscafn  17476  imasvscaval  17477  grpsubval  18893  isghmOLD  19124  lactghmga  19311  efgmval  19618  efgtval  19629  frgpup3lem  19683  dvrval  20288  frlmval  21633  psrvsca  21834  mat1comp  22303  mamulid  22304  mamurid  22305  madufval  22500  xkococnlem  23522  xkococn  23523  cnextval  23924  dscmet  24436  cncfval  24757  htpycom  24851  htpyid  24852  phtpycom  24863  phtpyid  24864  ehl1eudisval  25297  logbval  26652  addsval  27845  subsval  27940  mulsval  27988  divsval  28068  seqsval  28158  om2noseqrdg  28174  noseqrdgsuc  28178  seqsp1  28181  expsval  28287  isismt  28437  clwwlknon  29992  clwwlk0on0  29994  grpodivval  30437  ipval  30605  lnoval  30654  nmoofval  30664  bloval  30683  0ofval  30689  ajfval  30711  hvsubval  30918  hosmval  31637  hommval  31638  hodmval  31639  hfsmval  31640  hfmmval  31641  kbfval  31854  opsqrlem3  32044  dpval  32783  xdivval  32812  smatrcl  33759  smatlem  33760  mdetpmtr12  33788  pstmfval  33859  sxval  34153  ismbfm  34214  dya2iocival  34237  sitgval  34296  sitmval  34313  oddpwdcv  34319  ballotlemgval  34488  vtsval  34601  cvmlift2lem4  35266  icoreval  37314  metf1o  37722  heiborlem3  37780  heiborlem6  37783  heiborlem8  37785  heibor  37788  ldualvs  39103  tendopl  40743  cdlemkuu  40862  dvavsca  40984  dvhvaddval  41057  dvhvscaval  41066  hlhilipval  41916  resubval  42328  redivvald  42403  prjspnval  42577  rrx2xpref1o  48680  fuco22natlem  49307  functhinclem1  49406