Theorem ovmpoa 7605

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488  (class class class)co 7448   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  ovmpot  7611  1st2val  8058  2nd2val  8059  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  cantnffval  9732  cantnfsuc  9739  fseqenlem1  10093  xaddval  13285  xmulval  13287  fzoval  13717  expval  14114  ccatfval  14621  splcl  14800  cshfn  14838  bpolylem  16096  ruclem1  16279  sadfval  16498  sadcp1  16501  smufval  16523  smupp1  16526  eucalgval2  16628  pcval  16891  pc0  16901  vdwapval  17020  pwsval  17546  xpsfval  17626  xpsval  17630  rescval  17888  isfunc  17928  isfull  17977  isfth  17981  natfval  18014  catcisolem  18177  xpchom  18249  1stfval  18260  2ndfval  18263  yonedalem3a  18344  yonedainv  18351  plusfval  18685  ismgmhm  18734  ismhm  18820  mulgval  19111  eqgfval  19216  isghm  19255  isga  19331  subgga  19340  cayleylem1  19454  sylow1lem2  19641  isslw  19650  sylow2blem1  19662  sylow3lem1  19669  sylow3lem6  19674  frgpuptinv  19813  frgpup2  19818  isrhm  20504  scafval  20901  islmhm  21049  xrsdsval  21451  ipfval  21690  dsmmval  21777  psrmulfval  21986  mplval  22032  ltbval  22084  mpfrcl  22132  evlsval  22133  evlval  22142  mhpfval  22165  matval  22436  submafval  22606  mdetfval  22613  minmar1fval  22673  txval  23593  xkoval  23616  hmeofval  23787  flffval  24018  qustgplem  24150  dscmet  24606  dscopn  24607  tngval  24673  nmofval  24756  nghmfval  24764  isnmhm  24788  htpyco1  25029  htpycc  25031  phtpycc  25042  reparphti  25048  reparphtiOLD  25049  pcoval  25063  pcohtpylem  25071  pcorevlem  25078  dyadval  25646  itg1addlem3  25752  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  mdegfval  26121  quotval  26352  elqaalem2  26380  cxpval  26724  cxpcn3  26809  angval  26862  sgmval  27203  lgsval  27363  wwlksn  29870  wspthsn  29881  rusgrnumwwlklem  30003  clwwlkn  30058  2clwwlk  30379  numclwwlkovh0  30404  numclwwlkovq  30406  shsval  31344  sshjval  31382  faeval  34210  txsconnlem  35208  cvxsconn  35211  iscvm  35227  cvmliftlem5  35257  mpomulnzcnf  36265  rngohomval  37924  rngoisoval  37937  evlselv  42542  prjcrvfval  42586  rmxfval  42860  rmyfval  42861  mendplusg  43143  mendvsca  43148  mnringvald  44177  addrval  44435  subrval  44436  mulvval  44437  sigarval  46771  dmatALTval  48129  naryfval  48362