Theorem mpoeq3dva 7489

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 7478	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7415	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7415	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2796	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  mpoeq3ia  7490  mpoeq3dv  7491  fmpoco  8099  mapxpen  9162  cantnffval  9682  cantnfres  9696  sadfval  16476  smufval  16501  vdwapfval  16996  comfeq  17723  monpropd  17755  cofuval2  17905  cofuass  17907  cofulid  17908  cofurid  17909  catcisolem  18128  prfval  18216  prf1st  18221  prf2nd  18222  1st2ndprf  18223  xpcpropd  18225  curf1  18242  curfuncf  18255  curf2ndf  18264  grpsubpropd2  19034  mulgpropd  19104  oppglsm  19628  subglsm  19659  lsmpropd  19663  gsumcom2  19961  gsumdixp  20284  funcrngcsetcALT  20606  psrvscafval  21913  evlslem4  22039  evlslem2  22042  psrplusgpropd  22176  mamures  22340  mpomatmul  22389  mamutpos  22401  dmatmul  22440  dmatcrng  22445  scmatscmiddistr  22451  scmatcrng  22464  1marepvmarrepid  22518  1marepvsma1  22526  mdetrsca2  22547  mdetrlin2  22550  mdetunilem5  22559  mdetunilem6  22560  mdetunilem7  22561  mdetunilem8  22562  mdetunilem9  22563  maduval  22581  maducoeval  22582  maducoeval2  22583  madugsum  22586  madurid  22587  smadiadetglem2  22615  cramerimplem2  22627  mat2pmatghm  22673  mat2pmatmul  22674  m2cpminvid  22696  m2cpminvid2  22698  decpmatid  22713  decpmatmulsumfsupp  22716  monmatcollpw  22722  pmatcollpwscmatlem2  22733  mp2pm2mplem3  22751  mp2pm2mplem4  22752  pm2mpghm  22759  pm2mpmhmlem1  22761  ptval2  23544  cnmpt2t  23616  cnmpt22  23617  cnmptcom  23621  cnmptk2  23629  cnmpt2plusg  24031  istgp2  24034  prdstmdd  24067  cnmpt2vsca  24138  cnmpt2ds  24788  cnmpopc  24878  cnmpt2ip  25205  rrxds  25350  rrxmfval  25363  elntg2  28969  nvmfval  30630  elrgspnlem2  33243  fedgmullem2  33675  mdetpmtr12  33861  madjusmdetlem1  33863  pstmval  33931  sseqval  34425  cvmlift2lem6  35335  cvmlift2lem7  35336  cvmlift2lem12  35341  matunitlindflem1  37645  dvhfvadd  41115  fmpocos  42252  2arymaptfo  48614  rrxlinesc  48695  isofval2  48982  tposcurf1  49190  diag1  49195  precofvalALT  49259