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

Theorem mpt2eq3dva 6617
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 1258 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2620 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 671 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 6607 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpt2 6554 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpt2 6554 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2669 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031   = wceq 1475  wcel 1977  {coprab 6550  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-3an 1033  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:  mpt2eq3ia  6618  mpt2eq3dv  6619  ofeq  6797  fmpt2co  7147  mapxpen  8011  cantnffval  8443  cantnfres  8457  sadfval  15012  smufval  15037  vdwapfval  15513  comfeq  16189  monpropd  16220  cofuval2  16370  cofuass  16372  cofulid  16373  cofurid  16374  catcisolem  16579  prfval  16662  prf1st  16667  prf2nd  16668  1st2ndprf  16669  xpcpropd  16671  curf1  16688  curfuncf  16701  curf2ndf  16710  grpsubpropd2  17344  mulgpropd  17407  oppglsm  17880  subglsm  17909  lsmpropd  17913  gsumcom2  18197  gsumdixp  18432  psrvscafval  19211  evlslem4  19329  evlslem2  19333  psrplusgpropd  19427  mamures  20015  mpt2matmul  20071  mamutpos  20083  dmatmul  20122  dmatcrng  20127  scmatscmiddistr  20133  scmatcrng  20146  1marepvmarrepid  20200  1marepvsma1  20208  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  mdetunilem6  20242  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  maduval  20263  maducoeval  20264  maducoeval2  20265  madugsum  20268  madurid  20269  smadiadetglem2  20297  cramerimplem2  20309  mat2pmatghm  20354  mat2pmatmul  20355  m2cpminvid  20377  m2cpminvid2  20379  decpmatid  20394  decpmatmulsumfsupp  20397  monmatcollpw  20403  pmatcollpwscmatlem2  20414  mp2pm2mplem3  20432  mp2pm2mplem4  20433  pm2mpghm  20440  pm2mpmhmlem1  20442  ptval2  21214  cnmpt2t  21286  cnmpt22  21287  cnmptcom  21291  cnmptk2  21299  cnmpt2plusg  21702  istgp2  21705  prdstmdd  21737  cnmpt2vsca  21808  cnmpt2ds  22454  cnmpt2pc  22535  cnmpt2ip  22855  rrxds  22989  rrxmfval  22997  nvmfval  26883  mdetpmtr12  29219  madjusmdetlem1  29221  pstmval  29266  sseqval  29777  cvmlift2lem6  30544  cvmlift2lem7  30545  cvmlift2lem12  30550  matunitlindflem1  32575  dvhfvadd  35398  funcrngcsetcALT  41791
  Copyright terms: Public domain W3C validator