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

Theorem mpt2eq3dva 6866
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 1113 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2781 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 568 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 6856 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpt2 6798 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpt2 6798 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2830 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  {coprab 6794  cmpt2 6795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-oprab 6797  df-mpt2 6798
This theorem is referenced by:  mpt2eq3ia  6867  mpt2eq3dv  6868  ofeq  7046  fmpt2co  7411  mapxpen  8282  cantnffval  8724  cantnfres  8738  sadfval  15382  smufval  15407  vdwapfval  15882  comfeq  16573  monpropd  16604  cofuval2  16754  cofuass  16756  cofulid  16757  cofurid  16758  catcisolem  16963  prfval  17047  prf1st  17052  prf2nd  17053  1st2ndprf  17054  xpcpropd  17056  curf1  17073  curfuncf  17086  curf2ndf  17095  grpsubpropd2  17729  mulgpropd  17792  oppglsm  18264  subglsm  18293  lsmpropd  18297  gsumcom2  18581  gsumdixp  18817  psrvscafval  19605  evlslem4  19723  evlslem2  19727  psrplusgpropd  19821  mamures  20413  mpt2matmul  20470  mamutpos  20482  dmatmul  20521  dmatcrng  20526  scmatscmiddistr  20532  scmatcrng  20545  1marepvmarrepid  20599  1marepvsma1  20607  mdetrsca2  20628  mdetrlin2  20631  mdetunilem5  20640  mdetunilem6  20641  mdetunilem7  20642  mdetunilem8  20643  mdetunilem9  20644  maduval  20662  maducoeval  20663  maducoeval2  20664  madugsum  20667  madurid  20668  smadiadetglem2  20697  cramerimplem2  20710  mat2pmatghm  20755  mat2pmatmul  20756  m2cpminvid  20778  m2cpminvid2  20780  decpmatid  20795  decpmatmulsumfsupp  20798  monmatcollpw  20804  pmatcollpwscmatlem2  20815  mp2pm2mplem3  20833  mp2pm2mplem4  20834  pm2mpghm  20841  pm2mpmhmlem1  20843  ptval2  21625  cnmpt2t  21697  cnmpt22  21698  cnmptcom  21702  cnmptk2  21710  cnmpt2plusg  22112  istgp2  22115  prdstmdd  22147  cnmpt2vsca  22218  cnmpt2ds  22866  cnmpt2pc  22947  cnmpt2ip  23266  rrxds  23400  rrxmfval  23408  nvmfval  27839  mdetpmtr12  30231  madjusmdetlem1  30233  pstmval  30278  sseqval  30790  cvmlift2lem6  31628  cvmlift2lem7  31629  cvmlift2lem12  31634  matunitlindflem1  33738  dvhfvadd  36901  funcrngcsetcALT  42527
  Copyright terms: Public domain W3C validator