Theorem ovmpo 7552

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450  (class class class)co 7390   ∈ cmpo 7392

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  fvproj  8116  seqomlem1  8421  seqomlem4  8424  oav  8478  omv  8479  oev  8481  iunfictbso  10074  fin23lem12  10291  axdc4lem  10415  axcclem  10417  addpipq2  10896  mulpipq2  10899  subval  11419  divval  11846  cnref1o  12951  ixxval  13321  fzval  13477  modval  13840  om2uzrdg  13928  uzrdgsuci  13932  axdc4uzlem  13955  seqval  13984  seqp1  13988  bcval  14276  cnrecnv  15138  risefacval  15981  fallfacval  15982  gcdval  16473  lcmval  16569  imasvscafn  17507  imasvscaval  17508  grpsubval  18924  isghmOLD  19155  lactghmga  19342  efgmval  19649  efgtval  19660  frgpup3lem  19714  dvrval  20319  frlmval  21664  psrvsca  21865  mat1comp  22334  mamulid  22335  mamurid  22336  madufval  22531  xkococnlem  23553  xkococn  23554  cnextval  23955  dscmet  24467  cncfval  24788  htpycom  24882  htpyid  24883  phtpycom  24894  phtpyid  24895  ehl1eudisval  25328  logbval  26683  addsval  27876  subsval  27971  mulsval  28019  divsval  28099  seqsval  28189  om2noseqrdg  28205  noseqrdgsuc  28209  seqsp1  28212  expsval  28318  isismt  28468  clwwlknon  30026  clwwlk0on0  30028  grpodivval  30471  ipval  30639  lnoval  30688  nmoofval  30698  bloval  30717  0ofval  30723  ajfval  30745  hvsubval  30952  hosmval  31671  hommval  31672  hodmval  31673  hfsmval  31674  hfmmval  31675  kbfval  31888  opsqrlem3  32078  dpval  32817  xdivval  32846  smatrcl  33793  smatlem  33794  mdetpmtr12  33822  pstmfval  33893  sxval  34187  ismbfm  34248  dya2iocival  34271  sitgval  34330  sitmval  34347  oddpwdcv  34353  ballotlemgval  34522  vtsval  34635  cvmlift2lem4  35300  icoreval  37348  metf1o  37756  heiborlem3  37814  heiborlem6  37817  heiborlem8  37819  heibor  37822  ldualvs  39137  tendopl  40777  cdlemkuu  40896  dvavsca  41018  dvhvaddval  41091  dvhvscaval  41100  hlhilipval  41950  resubval  42362  redivvald  42437  prjspnval  42611  rrx2xpref1o  48711  fuco22natlem  49338  functhinclem1  49437