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

Theorem mpt2eq3dva 6885
Description: Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
Hypothesis
Ref Expression
mpt2eq3dva.1 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
Assertion
Ref Expression
mpt2eq3dva (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpt2eq3dva
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpt2eq3dva.1 . . . . . 6 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
213expb 1114 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2770 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 676 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 6875 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpt2 6819 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpt2 6819 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2819 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2139  {coprab 6815  cmpt2 6816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-oprab 6818  df-mpt2 6819
This theorem is referenced by:  mpt2eq3ia  6886  mpt2eq3dv  6887  ofeq  7065  fmpt2co  7429  mapxpen  8293  cantnffval  8735  cantnfres  8749  sadfval  15396  smufval  15421  vdwapfval  15897  comfeq  16587  monpropd  16618  cofuval2  16768  cofuass  16770  cofulid  16771  cofurid  16772  catcisolem  16977  prfval  17060  prf1st  17065  prf2nd  17066  1st2ndprf  17067  xpcpropd  17069  curf1  17086  curfuncf  17099  curf2ndf  17108  grpsubpropd2  17742  mulgpropd  17805  oppglsm  18277  subglsm  18306  lsmpropd  18310  gsumcom2  18594  gsumdixp  18829  psrvscafval  19612  evlslem4  19730  evlslem2  19734  psrplusgpropd  19828  mamures  20418  mpt2matmul  20474  mamutpos  20486  dmatmul  20525  dmatcrng  20530  scmatscmiddistr  20536  scmatcrng  20549  1marepvmarrepid  20603  1marepvsma1  20611  mdetrsca2  20632  mdetrlin2  20635  mdetunilem5  20644  mdetunilem6  20645  mdetunilem7  20646  mdetunilem8  20647  mdetunilem9  20648  maduval  20666  maducoeval  20667  maducoeval2  20668  madugsum  20671  madurid  20672  smadiadetglem2  20700  cramerimplem2  20712  mat2pmatghm  20757  mat2pmatmul  20758  m2cpminvid  20780  m2cpminvid2  20782  decpmatid  20797  decpmatmulsumfsupp  20800  monmatcollpw  20806  pmatcollpwscmatlem2  20817  mp2pm2mplem3  20835  mp2pm2mplem4  20836  pm2mpghm  20843  pm2mpmhmlem1  20845  ptval2  21626  cnmpt2t  21698  cnmpt22  21699  cnmptcom  21703  cnmptk2  21711  cnmpt2plusg  22113  istgp2  22116  prdstmdd  22148  cnmpt2vsca  22219  cnmpt2ds  22867  cnmpt2pc  22948  cnmpt2ip  23267  rrxds  23401  rrxmfval  23409  nvmfval  27829  mdetpmtr12  30221  madjusmdetlem1  30223  pstmval  30268  sseqval  30780  cvmlift2lem6  31618  cvmlift2lem7  31619  cvmlift2lem12  31624  matunitlindflem1  33736  dvhfvadd  36900  funcrngcsetcALT  42527
  Copyright terms: Public domain W3C validator