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

Theorem mpt2eq3dva 6672
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 1263 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2631 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 672 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 6662 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpt2 6609 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpt2 6609 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2680 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  {coprab 6605  cmpt2 6606
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-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-oprab 6608  df-mpt2 6609
This theorem is referenced by:  mpt2eq3ia  6673  mpt2eq3dv  6674  ofeq  6852  fmpt2co  7205  mapxpen  8070  cantnffval  8504  cantnfres  8518  sadfval  15098  smufval  15123  vdwapfval  15599  comfeq  16287  monpropd  16318  cofuval2  16468  cofuass  16470  cofulid  16471  cofurid  16472  catcisolem  16677  prfval  16760  prf1st  16765  prf2nd  16766  1st2ndprf  16767  xpcpropd  16769  curf1  16786  curfuncf  16799  curf2ndf  16808  grpsubpropd2  17442  mulgpropd  17505  oppglsm  17978  subglsm  18007  lsmpropd  18011  gsumcom2  18295  gsumdixp  18530  psrvscafval  19309  evlslem4  19427  evlslem2  19431  psrplusgpropd  19525  mamures  20115  mpt2matmul  20171  mamutpos  20183  dmatmul  20222  dmatcrng  20227  scmatscmiddistr  20233  scmatcrng  20246  1marepvmarrepid  20300  1marepvsma1  20308  mdetrsca2  20329  mdetrlin2  20332  mdetunilem5  20341  mdetunilem6  20342  mdetunilem7  20343  mdetunilem8  20344  mdetunilem9  20345  maduval  20363  maducoeval  20364  maducoeval2  20365  madugsum  20368  madurid  20369  smadiadetglem2  20397  cramerimplem2  20409  mat2pmatghm  20454  mat2pmatmul  20455  m2cpminvid  20477  m2cpminvid2  20479  decpmatid  20494  decpmatmulsumfsupp  20497  monmatcollpw  20503  pmatcollpwscmatlem2  20514  mp2pm2mplem3  20532  mp2pm2mplem4  20533  pm2mpghm  20540  pm2mpmhmlem1  20542  ptval2  21314  cnmpt2t  21386  cnmpt22  21387  cnmptcom  21391  cnmptk2  21399  cnmpt2plusg  21802  istgp2  21805  prdstmdd  21837  cnmpt2vsca  21908  cnmpt2ds  22554  cnmpt2pc  22635  cnmpt2ip  22955  rrxds  23089  rrxmfval  23097  nvmfval  27345  mdetpmtr12  29670  madjusmdetlem1  29672  pstmval  29717  sseqval  30228  cvmlift2lem6  30995  cvmlift2lem7  30996  cvmlift2lem12  31001  matunitlindflem1  33034  dvhfvadd  35857  funcrngcsetcALT  41284
  Copyright terms: Public domain W3C validator