Theorem ovmpoa 7342

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  Vcvv 3398  (class class class)co 7191   ∈ cmpo 7193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-iota 6316  df-fun 6360  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196

This theorem is referenced by:  1st2val  7767  2nd2val  7768  cantnffval  9256  cantnfsuc  9263  fseqenlem1  9603  xaddval  12778  xmulval  12780  fzoval  13209  expval  13602  ccatfval  14093  splcl  14282  cshfn  14320  bpolylem  15573  ruclem1  15755  sadfval  15974  sadcp1  15977  smufval  15999  smupp1  16002  eucalgval2  16101  pcval  16360  pc0  16370  vdwapval  16489  pwsval  16945  xpsfval  17025  xpsval  17029  rescval  17286  isfunc  17324  isfull  17371  isfth  17375  natfval  17407  catcisolem  17570  xpchom  17641  1stfval  17652  2ndfval  17655  yonedalem3a  17736  yonedainv  17743  plusfval  18075  ismhm  18174  mulgval  18446  eqgfval  18546  isga  18639  subgga  18648  cayleylem1  18758  sylow1lem2  18942  isslw  18951  sylow2blem1  18963  sylow3lem1  18970  sylow3lem6  18975  frgpuptinv  19115  frgpup2  19120  isrhm  19695  scafval  19872  islmhm  20018  xrsdsval  20361  ipfval  20565  dsmmval  20650  psrmulfval  20864  mplval  20907  ltbval  20954  mpfrcl  20999  evlsval  21000  evlval  21009  mhpfval  21033  matval  21262  submafval  21430  mdetfval  21437  minmar1fval  21497  txval  22415  xkoval  22438  hmeofval  22609  flffval  22840  qustgplem  22972  dscmet  23424  dscopn  23425  tngval  23491  nmofval  23566  nghmfval  23574  isnmhm  23598  htpyco1  23829  htpycc  23831  phtpycc  23842  reparphti  23848  pcoval  23862  pcohtpylem  23870  pcorevlem  23877  dyadval  24443  itg1addlem3  24549  itg1addlem4  24550  itg1addlem4OLD  24551  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  mdegfval  24914  quotval  25139  elqaalem2  25167  cxpval  25506  cxpcn3  25588  angval  25638  sgmval  25978  lgsval  26136  wwlksn  27875  wspthsn  27886  rusgrnumwwlklem  28008  clwwlkn  28063  2clwwlk  28384  numclwwlkovh0  28409  numclwwlkovq  28411  shsval  29347  sshjval  29385  faeval  31880  txsconnlem  32869  cvxsconn  32872  iscvm  32888  cvmliftlem5  32918  rngohomval  35808  rngoisoval  35821  rmxfval  40370  rmyfval  40371  mendplusg  40655  mendvsca  40660  mnringvald  41445  addrval  41698  subrval  41699  mulvval  41700  sigarval  43981  ismgmhm  44953  dmatALTval  45357  naryfval  45590