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

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

Proof of Theorem mpoeq3dva
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpoeq3dva.1 . . . . . 6 ((𝜑𝑥𝐴𝑦𝐵) → 𝐶 = 𝐷)
213expb 1113 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2805 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 579 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 7079 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpo 7021 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpo 7021 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2856 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080   = wceq 1522  wcel 2081  {coprab 7017  cmpo 7018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-oprab 7020  df-mpo 7021
This theorem is referenced by:  mpoeq3ia  7090  mpoeq3dv  7091  ofeq  7269  fmpoco  7646  mapxpen  8530  cantnffval  8972  cantnfres  8986  sadfval  15634  smufval  15659  vdwapfval  16136  comfeq  16805  monpropd  16836  cofuval2  16986  cofuass  16988  cofulid  16989  cofurid  16990  catcisolem  17195  prfval  17278  prf1st  17283  prf2nd  17284  1st2ndprf  17285  xpcpropd  17287  curf1  17304  curfuncf  17317  curf2ndf  17326  grpsubpropd2  17962  mulgpropd  18023  oppglsm  18497  subglsm  18526  lsmpropd  18530  gsumcom2  18815  gsumdixp  19049  psrvscafval  19858  evlslem4  19975  evlslem2  19979  psrplusgpropd  20087  mamures  20683  mpomatmul  20739  mamutpos  20751  dmatmul  20790  dmatcrng  20795  scmatscmiddistr  20801  scmatcrng  20814  1marepvmarrepid  20868  1marepvsma1  20876  mdetrsca2  20897  mdetrlin2  20900  mdetunilem5  20909  mdetunilem6  20910  mdetunilem7  20911  mdetunilem8  20912  mdetunilem9  20913  maduval  20931  maducoeval  20932  maducoeval2  20933  madugsum  20936  madurid  20937  smadiadetglem2  20965  cramerimplem2  20977  mat2pmatghm  21022  mat2pmatmul  21023  m2cpminvid  21045  m2cpminvid2  21047  decpmatid  21062  decpmatmulsumfsupp  21065  monmatcollpw  21071  pmatcollpwscmatlem2  21082  mp2pm2mplem3  21100  mp2pm2mplem4  21101  pm2mpghm  21108  pm2mpmhmlem1  21110  ptval2  21893  cnmpt2t  21965  cnmpt22  21966  cnmptcom  21970  cnmptk2  21978  cnmpt2plusg  22380  istgp2  22383  prdstmdd  22415  cnmpt2vsca  22486  cnmpt2ds  23134  cnmpopc  23215  cnmpt2ip  23534  rrxds  23679  rrxmfval  23692  elntg2  26454  nvmfval  28112  fedgmullem2  30630  mdetpmtr12  30705  madjusmdetlem1  30707  pstmval  30752  sseqval  31263  cvmlift2lem6  32164  cvmlift2lem7  32165  cvmlift2lem12  32170  matunitlindflem1  34438  dvhfvadd  37777  funcrngcsetcALT  43768  rrxlinesc  44223
  Copyright terms: Public domain W3C validator