Theorem ovmpoa 7547

Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)

Hypotheses

Ref	Expression
ovmpoga.1	⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
ovmpoga.2	⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
ovmpoa.4	⊢ 𝑆 ∈ V

Assertion

Ref	Expression
ovmpoa	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem ovmpoa

Step	Hyp	Ref	Expression
1		ovmpoa.4	. 2 ⊢ 𝑆 ∈ V
2		ovmpoga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
3		ovmpoga.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
4	2, 3	ovmpoga 7546	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ V) → (𝐴𝐹𝐵) = 𝑆)
5	1, 4	mp3an3 1470	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453  (class class class)co 7392   ∈ cmpo 7394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397

This theorem is referenced by:  ovmpot  7553  1st2val  7994  2nd2val  7995  mptmpoopabbrd  8057  cantnffval  9615  cantnfsuc  9622  fseqenlem1  9977  xaddval  13223  xmulval  13225  fzoval  13662  expval  14073  ccatfval  14583  splcl  14762  cshfn  14800  bpolylem  16061  ruclem1  16246  sadfval  16469  sadcp1  16472  smufval  16494  smupp1  16497  eucalgval2  16598  pcval  16863  pc0  16873  vdwapval  16992  pwsval  17498  xpsfval  17579  xpsval  17583  rescval  17843  isfunc  17880  isfull  17928  isfth  17932  natfval  17965  catcisolem  18126  xpchom  18195  1stfval  18206  2ndfval  18209  yonedalem3a  18289  yonedainv  18296  plusfval  18664  ismgmhm  18713  ismhm  18802  mulgval  19096  eqgfval  19200  isghm  19239  isga  19314  subgga  19323  cayleylem1  19435  sylow1lem2  19622  isslw  19631  sylow2blem1  19643  sylow3lem1  19650  sylow3lem6  19655  frgpuptinv  19794  frgpup2  19799  isrhm  20506  scafval  20928  islmhm  21074  xrsdsval  21443  ipfval  21681  dsmmval  21766  psrmulfval  21975  mplval  22020  ltbval  22076  mpfrcl  22118  evlsval  22119  evlval  22133  mhpfval  22183  matval  22451  submafval  22619  mdetfval  22626  minmar1fval  22686  txval  23604  xkoval  23627  hmeofval  23798  flffval  24029  qustgplem  24161  dscmet  24612  dscopn  24613  tngval  24679  nmofval  24754  nghmfval  24762  isnmhm  24786  htpyco1  25020  htpycc  25022  phtpycc  25033  reparphti  25039  pcoval  25053  pcohtpylem  25061  pcorevlem  25068  dyadval  25634  itg1addlem3  25740  itg1addlem4  25741  mbfi1fseqlem3  25759  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mbfi1fseqlem6  25762  mdegfval  26102  quotval  26333  elqaalem2  26361  cxpval  26706  cxpcn3  26790  angval  26843  sgmval  27183  lgsval  27342  wwlksn  29983  wspthsn  29994  rusgrnumwwlklem  30119  clwwlkn  30174  2clwwlk  30495  numclwwlkovh0  30520  numclwwlkovq  30522  shsval  31461  sshjval  31499  faeval  34504  txsconnlem  35554  cvxsconn  35557  iscvm  35573  cvmliftlem5  35603  mpomulnzcnf  36623  rngohomval  38427  rngoisoval  38440  evlselv  43135  prjcrvfval  43177  rmxfval  43445  rmyfval  43446  mendplusg  43723  mendvsca  43728  mnringvald  44753  addrval  45005  subrval  45006  mulvval  45007  sigarval  47388  dmatALTval  48986  naryfval  49214  discsubc  49649  oppfvalg  49711  upfval  49761  setc1onsubc  50187  lmdfval  50234  cmdfval  50235