Theorem mpoeq3dva 7488

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 1136	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2780	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 589	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7477	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7416	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7416	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2829	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  {coprab 7412   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  mpoeq3ia  7489  mpoeq3dv  7490  fmpoco  8089  mapxpen  9130  cantnffval  9631  cantnfres  9645  sadfval  16509  smufval  16534  vdwapfval  17030  comfeq  17761  monpropd  17793  cofuval2  17943  cofuass  17945  cofulid  17946  cofurid  17947  catcisolem  18166  prfval  18254  prf1st  18259  prf2nd  18260  1st2ndprf  18261  xpcpropd  18263  curf1  18280  curfuncf  18293  curf2ndf  18302  grpsubpropd2  19111  mulgpropd  19181  oppglsm  19711  subglsm  19742  lsmpropd  19746  gsumcom2  20044  gsumdixp  20399  funcrngcsetcALT  20725  psrvscafval  22066  evlslem4  22195  evlslem2  22198  psrplusgpropd  22363  mamures  22522  mpomatmul  22571  mamutpos  22583  dmatmul  22622  dmatcrng  22627  scmatscmiddistr  22633  scmatcrng  22646  1marepvmarrepid  22700  1marepvsma1  22708  mdetrsca2  22729  mdetrlin2  22732  mdetunilem5  22741  mdetunilem6  22742  mdetunilem7  22743  mdetunilem8  22744  mdetunilem9  22745  maduval  22763  maducoeval  22764  maducoeval2  22765  madugsum  22768  madurid  22769  smadiadetglem2  22797  cramerimplem2  22809  mat2pmatghm  22855  mat2pmatmul  22856  m2cpminvid  22878  m2cpminvid2  22880  decpmatid  22895  decpmatmulsumfsupp  22898  monmatcollpw  22904  pmatcollpwscmatlem2  22915  mp2pm2mplem3  22933  mp2pm2mplem4  22934  pm2mpghm  22941  pm2mpmhmlem1  22943  ptval2  23726  cnmpt2t  23798  cnmpt22  23799  cnmptcom  23803  cnmptk2  23811  cnmpt2plusg  24213  istgp2  24216  prdstmdd  24249  cnmpt2vsca  24320  cnmpt2ds  24969  cnmpopc  25055  cnmpt2ip  25375  rrxds  25520  rrxmfval  25533  elntg2  29275  nvmfval  30936  elrgspnlem2  33503  fedgmullem2  33964  mdetpmtr12  34159  madjusmdetlem1  34161  pstmval  34229  sseqval  34722  cvmlift2lem6  35698  cvmlift2lem7  35699  cvmlift2lem12  35704  matunitlindflem1  38154  dvhfvadd  41754  fmpocos  42893  2arymaptfo  49318  rrxlinesc  49399  isofval2  49694  oppc1stf  49950  oppc2ndf  49951  tposcurf1  49961  diag1  49966  precofvalALT  50030