Theorem ovmpoa 7575

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450  (class class class)co 7420   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425

This theorem is used by:  ovmpot  7581  1st2val  8029  2nd2val  8030  mptmpoopabbrd  8094  cantnffval  9667  cantnfsuc  9674  fseqenlem1  10106  xaddval  13356  xmulval  13358  fzoval  13797  expval  14209  ccatfval  14721  splcl  14905  cshfn  14945  bpolylem  16219  ruclem1  16404  sadfval  16627  sadcp1  16630  smufval  16652  smupp1  16655  eucalgval2  16761  pcval  17027  pc0  17037  vdwapval  17156  pwsval  17662  xpsfval  17743  xpsval  17747  rescval  18007  isfunc  18044  isfull  18092  isfth  18096  natfval  18129  catcisolem  18290  xpchom  18359  1stfval  18370  2ndfval  18373  yonedalem3a  18453  yonedainv  18460  plusfval  18828  ismgmhm  18890  ismhm  18985  mulgval  19286  eqgfval  19393  isghm  19435  isga  19510  subgga  19519  cayleylem1  19631  sylow1lem2  19818  isslw  19827  sylow2blem1  19839  sylow3lem1  19846  sylow3lem6  19851  frgpuptinv  19990  frgpup2  19995  rhmval0  20710  isrhm  20714  scafval  21161  islmhm  21307  xrsdsval  21722  ipfval  21960  dsmmval  22045  psrmulfval  22256  mplval  22301  ltbval  22357  mpfrcl  22399  evlsval  22400  evlval  22414  mhpfval  22464  matval  22731  submafval  22899  mdetfval  22906  minmar1fval  22966  txval  23888  xkoval  23911  hmeofval  24082  flffval  24313  qustgplem  24445  dscmet  24896  dscopn  24897  tngval  24963  nmofval  25038  nghmfval  25046  isnmhm  25070  htpyco1  25304  htpycc  25306  phtpycc  25317  reparphti  25323  pcoval  25337  pcohtpylem  25345  pcorevlem  25352  dyadval  25918  itg1addlem3  26024  itg1addlem4  26025  mbfi1fseqlem3  26043  mbfi1fseqlem4  26044  mbfi1fseqlem5  26045  mbfi1fseqlem6  26046  mdegfval  26385  quotval  26618  elqaalem2  26648  cxpval  26997  cxpcn3  27081  angval  27134  sgmval  27474  lgsval  27633  wwlksn  30431  wspthsn  30442  rusgrnumwwlklem  30567  clwwlkn  30622  2clwwlk  30953  numclwwlkovh0  30978  numclwwlkovq  30980  shsval  31919  sshjval  31957  faeval  34925  txsconnlem  36091  cvxsconn  36094  iscvm  36110  cvmliftlem5  36140  mpomulnzcnf  37180  rngohomval  38991  rngoisoval  39004  evlselv  43710  prjcrvfval  43760  rmxfval  44004  rmyfval  44005  mendplusg  44277  mendvsca  44282  mnringvald  45304  addrval  45541  subrval  45542  mulvval  45543  sigarval  47953  dmatALTval  49605  naryfval  49833  discsubc  50271  oppfvalg  50335  upfval  50385  setc1onsubc  50833  parhomval  50836  parhomidval  50839  lmdfval  50925  cmdfval  50926