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

Theorem mpoeq3dva 7220
 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 1117 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶 = 𝐷)
32eqeq2d 2809 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = 𝐶𝑧 = 𝐷))
43pm5.32da 582 . . 3 (𝜑 → (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)))
54oprabbidv 7209 . 2 (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)})
6 df-mpo 7150 . 2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
7 df-mpo 7150 . 2 (𝑥𝐴, 𝑦𝐵𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐷)}
85, 6, 73eqtr4g 2858 1 (𝜑 → (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {coprab 7146   ∈ cmpo 7147 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-oprab 7149  df-mpo 7150 This theorem is referenced by:  mpoeq3ia  7221  mpoeq3dv  7222  ofeq  7402  fmpoco  7786  mapxpen  8685  cantnffval  9128  cantnfres  9142  sadfval  15811  smufval  15836  vdwapfval  16317  comfeq  16988  monpropd  17019  cofuval2  17169  cofuass  17171  cofulid  17172  cofurid  17173  catcisolem  17378  prfval  17461  prf1st  17466  prf2nd  17467  1st2ndprf  17468  xpcpropd  17470  curf1  17487  curfuncf  17500  curf2ndf  17509  grpsubpropd2  18218  mulgpropd  18282  oppglsm  18780  subglsm  18812  lsmpropd  18816  gsumcom2  19109  gsumdixp  19376  psrvscafval  20664  evlslem4  20783  evlslem2  20788  psrplusgpropd  20906  mamures  21038  mpomatmul  21092  mamutpos  21104  dmatmul  21143  dmatcrng  21148  scmatscmiddistr  21154  scmatcrng  21167  1marepvmarrepid  21221  1marepvsma1  21229  mdetrsca2  21250  mdetrlin2  21253  mdetunilem5  21262  mdetunilem6  21263  mdetunilem7  21264  mdetunilem8  21265  mdetunilem9  21266  maduval  21284  maducoeval  21285  maducoeval2  21286  madugsum  21289  madurid  21290  smadiadetglem2  21318  cramerimplem2  21330  mat2pmatghm  21376  mat2pmatmul  21377  m2cpminvid  21399  m2cpminvid2  21401  decpmatid  21416  decpmatmulsumfsupp  21419  monmatcollpw  21425  pmatcollpwscmatlem2  21436  mp2pm2mplem3  21454  mp2pm2mplem4  21455  pm2mpghm  21462  pm2mpmhmlem1  21464  ptval2  22247  cnmpt2t  22319  cnmpt22  22320  cnmptcom  22324  cnmptk2  22332  cnmpt2plusg  22734  istgp2  22737  prdstmdd  22770  cnmpt2vsca  22841  cnmpt2ds  23489  cnmpopc  23574  cnmpt2ip  23893  rrxds  24038  rrxmfval  24051  elntg2  26823  nvmfval  28471  fedgmullem2  31180  mdetpmtr12  31244  madjusmdetlem1  31246  pstmval  31314  sseqval  31822  cvmlift2lem6  32734  cvmlift2lem7  32735  cvmlift2lem12  32740  matunitlindflem1  35204  dvhfvadd  38538  funcrngcsetcALT  44791  2arymaptfo  45234  rrxlinesc  45315
 Copyright terms: Public domain W3C validator