Theorem ovmpoa 7305

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Vcvv 3494  (class class class)co 7156   ∈ cmpo 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  1st2val  7717  2nd2val  7718  cantnffval  9126  cantnfsuc  9133  fseqenlem1  9450  xaddval  12617  xmulval  12619  fzoval  13040  expval  13432  ccatfval  13925  splcl  14114  cshfn  14152  bpolylem  15402  ruclem1  15584  sadfval  15801  sadcp1  15804  smufval  15826  smupp1  15829  eucalgval2  15925  pcval  16181  pc0  16191  vdwapval  16309  pwsval  16759  xpsfval  16839  xpsval  16843  rescval  17097  isfunc  17134  isfull  17180  isfth  17184  natfval  17216  catcisolem  17366  xpchom  17430  1stfval  17441  2ndfval  17444  yonedalem3a  17524  yonedainv  17531  plusfval  17859  ismhm  17958  mulgval  18228  eqgfval  18328  isga  18421  subgga  18430  cayleylem1  18540  sylow1lem2  18724  isslw  18733  sylow2blem1  18745  sylow3lem1  18752  sylow3lem6  18757  frgpuptinv  18897  frgpup2  18902  isrhm  19473  scafval  19653  islmhm  19799  psrmulfval  20165  mplval  20208  ltbval  20252  mpfrcl  20298  evlsval  20299  evlval  20308  xrsdsval  20589  ipfval  20793  dsmmval  20878  matval  21020  submafval  21188  mdetfval  21195  minmar1fval  21255  txval  22172  xkoval  22195  hmeofval  22366  flffval  22597  qustgplem  22729  dscmet  23182  dscopn  23183  tngval  23248  nmofval  23323  nghmfval  23331  isnmhm  23355  htpyco1  23582  htpycc  23584  phtpycc  23595  reparphti  23601  pcoval  23615  pcohtpylem  23623  pcorevlem  23630  dyadval  24193  itg1addlem3  24299  itg1addlem4  24300  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  mdegfval  24656  quotval  24881  elqaalem2  24909  cxpval  25247  cxpcn3  25329  angval  25379  sgmval  25719  lgsval  25877  wwlksn  27615  wspthsn  27626  rusgrnumwwlklem  27749  clwwlkn  27804  2clwwlk  28126  numclwwlkovh0  28151  numclwwlkovq  28153  shsval  29089  sshjval  29127  faeval  31505  txsconnlem  32487  cvxsconn  32490  iscvm  32506  cvmliftlem5  32536  rngohomval  35257  rngoisoval  35270  rmxfval  39550  rmyfval  39551  mendplusg  39835  mendvsca  39840  addrval  40847  subrval  40848  mulvval  40849  sigarval  43156  ismgmhm  44099  dmatALTval  44504