MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2eq123dv Structured version   Visualization version   GIF version

Theorem mpt2eq123dv 6615
Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
Hypotheses
Ref Expression
mpt2eq123dv.1 (𝜑𝐴 = 𝐷)
mpt2eq123dv.2 (𝜑𝐵 = 𝐸)
mpt2eq123dv.3 (𝜑𝐶 = 𝐹)
Assertion
Ref Expression
mpt2eq123dv (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpt2eq123dv
StepHypRef Expression
1 mpt2eq123dv.1 . 2 (𝜑𝐴 = 𝐷)
2 mpt2eq123dv.2 . . 3 (𝜑𝐵 = 𝐸)
32adantr 480 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
4 mpt2eq123dv.3 . . 3 (𝜑𝐶 = 𝐹)
54adantr 480 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
61, 3, 5mpt2eq123dva 6614 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  cmpt2 6551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-oprab 6553  df-mpt2 6554
This theorem is referenced by:  mpt2eq123i  6616  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvv  7144  prdsval  15938  imasval  15994  imasvscaval  16021  homffval  16173  homfeq  16177  comfffval  16181  comffval  16182  comfffval2  16184  comffval2  16185  comfeq  16189  oppcval  16196  monfval  16215  sectffval  16233  invffval  16241  isofn  16258  cofuval  16365  natfval  16429  fucval  16441  fucco  16445  coafval  16537  setcval  16550  setcco  16556  catcval  16569  catcco  16574  estrcval  16587  estrcco  16593  xpcval  16640  xpchomfval  16642  xpccofval  16645  1stfval  16654  2ndfval  16657  prfval  16662  evlfval  16680  evlf2  16681  curfval  16686  hofval  16715  hof2fval  16718  plusffval  17070  grpsubfval  17287  grpsubpropd  17343  mulgfval  17365  mulgpropd  17407  symgval  17622  lsmfval  17876  pj1fval  17930  efgtf  17958  prdsmgp  18433  dvrfval  18507  scaffval  18704  psrval  19183  ipffval  19812  phssip  19822  frlmip  19936  mamufval  20010  mvmulfval  20167  marrepfval  20185  marepvfval  20190  submafval  20204  submaval  20206  madufval  20262  minmar1fval  20271  mat2pmatfval  20347  cpm2mfval  20373  decpmatval0  20388  decpmatval  20389  pmatcollpw3lem  20407  xkoval  21200  xkopt  21268  xpstopnlem1  21422  submtmd  21718  blfvalps  21998  ishtpy  22579  isphtpy  22588  pcofval  22618  rrxip  22986  q1pval  23717  r1pval  23720  taylfval  23917  midf  25468  ismidb  25470  ttgval  25555  wlkon  26061  trlon  26070  pthon  26105  spthon  26112  is2wlkonot  26390  is2spthonot  26391  2wlkonot3v  26402  2spthonot3v  26403  grpodivfval  26772  dipfval  26941  submatres  29200  lmatval  29207  lmatcl  29210  qqhval  29346  sxval  29580  sitmval  29738  cndprobval  29822  mclsval  30714  csbfinxpg  32401  rrnval  32796  ldualset  33430  paddfval  34101  tgrpfset  35050  tgrpset  35051  erngfset  35105  erngset  35106  erngfset-rN  35113  erngset-rN  35114  dvafset  35310  dvaset  35311  dvhfset  35387  dvhset  35388  djaffvalN  35440  djafvalN  35441  djhffval  35703  djhfval  35704  hlhilset  36244  eldiophb  36338  mendval  36772  hoidmvval  39467  ovnhoi  39493  hspval  39499  hspmbllem2  39517  hoimbl  39521  mptmpt2opabbrd  40335  wwlksnon  41049  wspthsnon  41050  rngcvalALTV  41753  rngccoALTV  41780  funcrngcsetcALT  41791  ringcvalALTV  41799  ringccoALTV  41843  lincop  41991
  Copyright terms: Public domain W3C validator