Theorem mpoeq3dva 7473

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 1133	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2773	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 587	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7462	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7401	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7401	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2822	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  {coprab 7397   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-oprab 7400  df-mpo 7401

This theorem is referenced by:  mpoeq3ia  7474  mpoeq3dv  7475  fmpoco  8074  mapxpen  9115  cantnffval  9618  cantnfres  9632  sadfval  16486  smufval  16511  vdwapfval  17007  comfeq  17738  monpropd  17770  cofuval2  17920  cofuass  17922  cofulid  17923  cofurid  17924  catcisolem  18143  prfval  18231  prf1st  18236  prf2nd  18237  1st2ndprf  18238  xpcpropd  18240  curf1  18257  curfuncf  18270  curf2ndf  18279  grpsubpropd2  19088  mulgpropd  19158  oppglsm  19682  subglsm  19713  lsmpropd  19717  gsumcom2  20015  gsumdixp  20367  funcrngcsetcALT  20691  psrvscafval  22000  evlslem4  22129  evlslem2  22132  psrplusgpropd  22297  mamures  22457  mpomatmul  22506  mamutpos  22518  dmatmul  22557  dmatcrng  22562  scmatscmiddistr  22568  scmatcrng  22581  1marepvmarrepid  22635  1marepvsma1  22643  mdetrsca2  22664  mdetrlin2  22667  mdetunilem5  22676  mdetunilem6  22677  mdetunilem7  22678  mdetunilem8  22679  mdetunilem9  22680  maduval  22698  maducoeval  22699  maducoeval2  22700  madugsum  22703  madurid  22704  smadiadetglem2  22732  cramerimplem2  22744  mat2pmatghm  22790  mat2pmatmul  22791  m2cpminvid  22813  m2cpminvid2  22815  decpmatid  22830  decpmatmulsumfsupp  22833  monmatcollpw  22839  pmatcollpwscmatlem2  22850  mp2pm2mplem3  22868  mp2pm2mplem4  22869  pm2mpghm  22876  pm2mpmhmlem1  22878  ptval2  23661  cnmpt2t  23733  cnmpt22  23734  cnmptcom  23738  cnmptk2  23746  cnmpt2plusg  24148  istgp2  24151  prdstmdd  24184  cnmpt2vsca  24255  cnmpt2ds  24904  cnmpopc  24990  cnmpt2ip  25310  rrxds  25455  rrxmfval  25468  elntg2  29186  nvmfval  30847  elrgspnlem2  33424  fedgmullem2  33927  mdetpmtr12  34122  madjusmdetlem1  34124  pstmval  34192  sseqval  34685  cvmlift2lem6  35658  cvmlift2lem7  35659  cvmlift2lem12  35664  matunitlindflem1  38115  dvhfvadd  41715  fmpocos  42852  2arymaptfo  49276  rrxlinesc  49357  isofval2  49653  oppc1stf  49909  oppc2ndf  49910  tposcurf1  49920  diag1  49925  precofvalALT  49989