Theorem mpoeq3dva 7496

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 1138	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2776	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 590	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7485	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7424	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7424	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2825	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  {coprab 7420   ∈ cmpo 7421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-oprab 7423  df-mpo 7424

This theorem is used by:  mpoeq3ia  7497  mpoeq3dv  7498  fmpoco  8096  mapxpen  9138  cantnffval  9639  cantnfres  9653  sadfval  16532  smufval  16557  vdwapfval  17053  comfeq  17784  monpropd  17816  cofuval2  17966  cofuass  17968  cofulid  17969  cofurid  17970  catcisolem  18189  prfval  18277  prf1st  18282  prf2nd  18283  1st2ndprf  18284  xpcpropd  18286  curf1  18303  curfuncf  18316  curf2ndf  18325  grpsubpropd2  19156  mulgpropd  19226  oppglsm  19756  subglsm  19787  lsmpropd  19791  gsumcom2  20089  gsumdixp  20446  funcrngcsetcALT  20790  psrvscafval  22148  evlslem4  22277  evlslem2  22280  psrplusgpropd  22445  mamures  22604  mpomatmul  22653  mamutpos  22665  dmatmul  22704  dmatcrng  22709  scmatscmiddistr  22715  scmatcrng  22728  1marepvmarrepid  22782  1marepvsma1  22790  mdetrsca2  22811  mdetrlin2  22814  mdetunilem5  22823  mdetunilem6  22824  mdetunilem7  22825  mdetunilem8  22826  mdetunilem9  22827  maduval  22845  maducoeval  22846  maducoeval2  22847  madugsum  22850  madurid  22851  smadiadetglem2  22879  cramerimplem2  22891  mat2pmatghm  22937  mat2pmatmul  22938  m2cpminvid  22960  m2cpminvid2  22962  decpmatid  22977  decpmatmulsumfsupp  22980  monmatcollpw  22986  pmatcollpwscmatlem2  22997  mp2pm2mplem3  23015  mp2pm2mplem4  23016  pm2mpghm  23023  pm2mpmhmlem1  23025  ptval2  23809  cnmpt2t  23881  cnmpt22  23882  cnmptcom  23886  cnmptk2  23894  cnmpt2plusg  24296  istgp2  24299  prdstmdd  24332  cnmpt2vsca  24403  cnmpt2ds  25052  cnmpopc  25138  cnmpt2ip  25458  rrxds  25603  rrxmfval  25616  elntg2  29390  nvmfval  31067  elrgspnlem2  33627  fedgmullem2  34084  mdetpmtr12  34279  madjusmdetlem1  34281  pstmval  34349  sseqval  34843  cvmlift2lem6  35837  cvmlift2lem7  35838  cvmlift2lem12  35843  matunitlindflem1  38324  dvhfvadd  41923  fmpocos  43062  2arymaptfo  49491  rrxlinesc  49572  isofval2  49867  oppc1stf  50123  oppc2ndf  50124  tposcurf1  50134  diag1  50139  precofvalALT  50203