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

Theorem mpt2eq123dv 6677
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 481 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐸)
4 mpt2eq123dv.3 . . 3 (𝜑𝐶 = 𝐹)
54adantr 481 . 2 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐹)
61, 3, 5mpt2eq123dva 6676 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐷, 𝑦𝐸𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  cmpt2 6612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-oprab 6614  df-mpt2 6615
This theorem is referenced by:  mpt2eq123i  6678  mptmpt2opabbrd  7200  el2mpt2csbcl  7202  bropopvvv  7207  bropfvvvv  7209  prdsval  16047  imasval  16103  imasvscaval  16130  homffval  16282  homfeq  16286  comfffval  16290  comffval  16291  comfffval2  16293  comffval2  16294  comfeq  16298  oppcval  16305  monfval  16324  sectffval  16342  invffval  16350  isofn  16367  cofuval  16474  natfval  16538  fucval  16550  fucco  16554  coafval  16646  setcval  16659  setcco  16665  catcval  16678  catcco  16683  estrcval  16696  estrcco  16702  xpcval  16749  xpchomfval  16751  xpccofval  16754  1stfval  16763  2ndfval  16766  prfval  16771  evlfval  16789  evlf2  16790  curfval  16795  hofval  16824  hof2fval  16827  plusffval  17179  grpsubfval  17396  grpsubpropd  17452  mulgfval  17474  mulgpropd  17516  symgval  17731  lsmfval  17985  pj1fval  18039  efgtf  18067  prdsmgp  18542  dvrfval  18616  scaffval  18813  psrval  19294  ipffval  19925  phssip  19935  frlmip  20049  mamufval  20123  mvmulfval  20280  marrepfval  20298  marepvfval  20303  submafval  20317  submaval  20319  madufval  20375  minmar1fval  20384  mat2pmatfval  20460  cpm2mfval  20486  decpmatval0  20501  decpmatval  20502  pmatcollpw3lem  20520  xkoval  21313  xkopt  21381  xpstopnlem1  21535  submtmd  21831  blfvalps  22111  ishtpy  22694  isphtpy  22703  pcofval  22733  rrxip  23101  q1pval  23834  r1pval  23837  taylfval  24034  midf  25585  ismidb  25587  ttgval  25672  wwlksnon  26624  wspthsnon  26625  grpodivfval  27258  dipfval  27427  submatres  29678  lmatval  29685  lmatcl  29688  qqhval  29824  sxval  30058  sitmval  30216  cndprobval  30300  mclsval  31203  csbfinxpg  32892  rrnval  33293  ldualset  33927  paddfval  34598  tgrpfset  35547  tgrpset  35548  erngfset  35602  erngset  35603  erngfset-rN  35610  erngset-rN  35611  dvafset  35807  dvaset  35808  dvhfset  35884  dvhset  35885  djaffvalN  35937  djafvalN  35938  djhffval  36200  djhfval  36201  hlhilset  36741  eldiophb  36835  mendval  37269  hoidmvval  40124  ovnhoi  40150  hspval  40156  hspmbllem2  40174  hoimbl  40178  rngcvalALTV  41275  rngccoALTV  41302  funcrngcsetcALT  41313  ringcvalALTV  41321  ringccoALTV  41365  lincop  41511
  Copyright terms: Public domain W3C validator