Theorem mpoeq3dva 7446

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.

Step	Hyp	Ref	Expression
1		mpoeq3dva.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
2	1	3expb 1120	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2740	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 579	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7435	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7374	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7374	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2789	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {coprab 7370   ∈ cmpo 7371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  mpoeq3ia  7447  mpoeq3dv  7448  fmpoco  8051  mapxpen  9084  cantnffval  9592  cantnfres  9606  sadfval  16398  smufval  16423  vdwapfval  16918  comfeq  17643  monpropd  17675  cofuval2  17825  cofuass  17827  cofulid  17828  cofurid  17829  catcisolem  18048  prfval  18136  prf1st  18141  prf2nd  18142  1st2ndprf  18143  xpcpropd  18145  curf1  18162  curfuncf  18175  curf2ndf  18184  grpsubpropd2  18954  mulgpropd  19024  oppglsm  19548  subglsm  19579  lsmpropd  19583  gsumcom2  19881  gsumdixp  20204  funcrngcsetcALT  20526  psrvscafval  21833  evlslem4  21959  evlslem2  21962  psrplusgpropd  22096  mamures  22260  mpomatmul  22309  mamutpos  22321  dmatmul  22360  dmatcrng  22365  scmatscmiddistr  22371  scmatcrng  22384  1marepvmarrepid  22438  1marepvsma1  22446  mdetrsca2  22467  mdetrlin2  22470  mdetunilem5  22479  mdetunilem6  22480  mdetunilem7  22481  mdetunilem8  22482  mdetunilem9  22483  maduval  22501  maducoeval  22502  maducoeval2  22503  madugsum  22506  madurid  22507  smadiadetglem2  22535  cramerimplem2  22547  mat2pmatghm  22593  mat2pmatmul  22594  m2cpminvid  22616  m2cpminvid2  22618  decpmatid  22633  decpmatmulsumfsupp  22636  monmatcollpw  22642  pmatcollpwscmatlem2  22653  mp2pm2mplem3  22671  mp2pm2mplem4  22672  pm2mpghm  22679  pm2mpmhmlem1  22681  ptval2  23464  cnmpt2t  23536  cnmpt22  23537  cnmptcom  23541  cnmptk2  23549  cnmpt2plusg  23951  istgp2  23954  prdstmdd  23987  cnmpt2vsca  24058  cnmpt2ds  24708  cnmpopc  24798  cnmpt2ip  25124  rrxds  25269  rrxmfval  25282  elntg2  28888  nvmfval  30546  elrgspnlem2  33167  fedgmullem2  33599  mdetpmtr12  33788  madjusmdetlem1  33790  pstmval  33858  sseqval  34352  cvmlift2lem6  35268  cvmlift2lem7  35269  cvmlift2lem12  35274  matunitlindflem1  37583  dvhfvadd  41058  fmpocos  42195  2arymaptfo  48616  rrxlinesc  48697  isofval2  48994  oppc1stf  49250  oppc2ndf  49251  tposcurf1  49261  diag1  49266  precofvalALT  49330