Theorem mpoeq3dva 7511

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 2747	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 579	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7500	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7437	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7437	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2801	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {coprab 7433   ∈ cmpo 7434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-oprab 7436  df-mpo 7437

This theorem is referenced by:  mpoeq3ia  7512  mpoeq3dv  7513  fmpoco  8121  mapxpen  9184  cantnffval  9704  cantnfres  9718  sadfval  16490  smufval  16515  vdwapfval  17010  comfeq  17750  monpropd  17782  cofuval2  17933  cofuass  17935  cofulid  17936  cofurid  17937  catcisolem  18156  prfval  18245  prf1st  18250  prf2nd  18251  1st2ndprf  18252  xpcpropd  18254  curf1  18271  curfuncf  18284  curf2ndf  18293  grpsubpropd2  19065  mulgpropd  19135  oppglsm  19661  subglsm  19692  lsmpropd  19696  gsumcom2  19994  gsumdixp  20317  funcrngcsetcALT  20642  psrvscafval  21969  evlslem4  22101  evlslem2  22104  psrplusgpropd  22238  mamures  22402  mpomatmul  22453  mamutpos  22465  dmatmul  22504  dmatcrng  22509  scmatscmiddistr  22515  scmatcrng  22528  1marepvmarrepid  22582  1marepvsma1  22590  mdetrsca2  22611  mdetrlin2  22614  mdetunilem5  22623  mdetunilem6  22624  mdetunilem7  22625  mdetunilem8  22626  mdetunilem9  22627  maduval  22645  maducoeval  22646  maducoeval2  22647  madugsum  22650  madurid  22651  smadiadetglem2  22679  cramerimplem2  22691  mat2pmatghm  22737  mat2pmatmul  22738  m2cpminvid  22760  m2cpminvid2  22762  decpmatid  22777  decpmatmulsumfsupp  22780  monmatcollpw  22786  pmatcollpwscmatlem2  22797  mp2pm2mplem3  22815  mp2pm2mplem4  22816  pm2mpghm  22823  pm2mpmhmlem1  22825  ptval2  23610  cnmpt2t  23682  cnmpt22  23683  cnmptcom  23687  cnmptk2  23695  cnmpt2plusg  24097  istgp2  24100  prdstmdd  24133  cnmpt2vsca  24204  cnmpt2ds  24866  cnmpopc  24956  cnmpt2ip  25283  rrxds  25428  rrxmfval  25441  elntg2  29001  nvmfval  30664  elrgspnlem2  33248  fedgmullem2  33682  mdetpmtr12  33825  madjusmdetlem1  33827  pstmval  33895  sseqval  34391  cvmlift2lem6  35314  cvmlift2lem7  35315  cvmlift2lem12  35320  matunitlindflem1  37624  dvhfvadd  41094  fmpocos  42275  2arymaptfo  48580  rrxlinesc  48661  tposcurf1  49017  diag1  49022  precofvalALT  49086