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

Theorem mpoeq3dva 7288
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 1122 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2748 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 582 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 7277 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpo 7218 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpo 7218 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2803 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  {coprab 7214  cmpo 7215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-oprab 7217  df-mpo 7218
This theorem is referenced by:  mpoeq3ia  7289  mpoeq3dv  7290  ofeq  7471  fmpoco  7863  mapxpen  8812  cantnffval  9278  cantnfres  9292  sadfval  16011  smufval  16036  vdwapfval  16524  comfeq  17209  monpropd  17242  cofuval2  17393  cofuass  17395  cofulid  17396  cofurid  17397  catcisolem  17616  prfval  17706  prf1st  17711  prf2nd  17712  1st2ndprf  17713  xpcpropd  17716  curf1  17733  curfuncf  17746  curf2ndf  17755  grpsubpropd2  18469  mulgpropd  18533  oppglsm  19031  subglsm  19063  lsmpropd  19067  gsumcom2  19360  gsumdixp  19627  psrvscafval  20915  evlslem4  21034  evlslem2  21039  psrplusgpropd  21157  mamures  21289  mpomatmul  21343  mamutpos  21355  dmatmul  21394  dmatcrng  21399  scmatscmiddistr  21405  scmatcrng  21418  1marepvmarrepid  21472  1marepvsma1  21480  mdetrsca2  21501  mdetrlin2  21504  mdetunilem5  21513  mdetunilem6  21514  mdetunilem7  21515  mdetunilem8  21516  mdetunilem9  21517  maduval  21535  maducoeval  21536  maducoeval2  21537  madugsum  21540  madurid  21541  smadiadetglem2  21569  cramerimplem2  21581  mat2pmatghm  21627  mat2pmatmul  21628  m2cpminvid  21650  m2cpminvid2  21652  decpmatid  21667  decpmatmulsumfsupp  21670  monmatcollpw  21676  pmatcollpwscmatlem2  21687  mp2pm2mplem3  21705  mp2pm2mplem4  21706  pm2mpghm  21713  pm2mpmhmlem1  21715  ptval2  22498  cnmpt2t  22570  cnmpt22  22571  cnmptcom  22575  cnmptk2  22583  cnmpt2plusg  22985  istgp2  22988  prdstmdd  23021  cnmpt2vsca  23092  cnmpt2ds  23740  cnmpopc  23825  cnmpt2ip  24145  rrxds  24290  rrxmfval  24303  elntg2  27076  nvmfval  28725  fedgmullem2  31425  mdetpmtr12  31489  madjusmdetlem1  31491  pstmval  31559  sseqval  32067  cvmlift2lem6  32983  cvmlift2lem7  32984  cvmlift2lem12  32989  matunitlindflem1  35510  dvhfvadd  38842  funcrngcsetcALT  45230  2arymaptfo  45673  rrxlinesc  45754
  Copyright terms: Public domain W3C validator