Theorem mpoeq3dva 7423

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  {coprab 7347   ∈ cmpo 7348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  mpoeq3ia  7424  mpoeq3dv  7425  fmpoco  8025  mapxpen  9056  cantnffval  9553  cantnfres  9567  sadfval  16363  smufval  16388  vdwapfval  16883  comfeq  17612  monpropd  17644  cofuval2  17794  cofuass  17796  cofulid  17797  cofurid  17798  catcisolem  18017  prfval  18105  prf1st  18110  prf2nd  18111  1st2ndprf  18112  xpcpropd  18114  curf1  18131  curfuncf  18144  curf2ndf  18153  grpsubpropd2  18959  mulgpropd  19029  oppglsm  19554  subglsm  19585  lsmpropd  19589  gsumcom2  19887  gsumdixp  20237  funcrngcsetcALT  20556  psrvscafval  21885  evlslem4  22011  evlslem2  22014  psrplusgpropd  22148  mamures  22312  mpomatmul  22361  mamutpos  22373  dmatmul  22412  dmatcrng  22417  scmatscmiddistr  22423  scmatcrng  22436  1marepvmarrepid  22490  1marepvsma1  22498  mdetrsca2  22519  mdetrlin2  22522  mdetunilem5  22531  mdetunilem6  22532  mdetunilem7  22533  mdetunilem8  22534  mdetunilem9  22535  maduval  22553  maducoeval  22554  maducoeval2  22555  madugsum  22558  madurid  22559  smadiadetglem2  22587  cramerimplem2  22599  mat2pmatghm  22645  mat2pmatmul  22646  m2cpminvid  22668  m2cpminvid2  22670  decpmatid  22685  decpmatmulsumfsupp  22688  monmatcollpw  22694  pmatcollpwscmatlem2  22705  mp2pm2mplem3  22723  mp2pm2mplem4  22724  pm2mpghm  22731  pm2mpmhmlem1  22733  ptval2  23516  cnmpt2t  23588  cnmpt22  23589  cnmptcom  23593  cnmptk2  23601  cnmpt2plusg  24003  istgp2  24006  prdstmdd  24039  cnmpt2vsca  24110  cnmpt2ds  24759  cnmpopc  24849  cnmpt2ip  25175  rrxds  25320  rrxmfval  25333  elntg2  28963  nvmfval  30624  elrgspnlem2  33210  fedgmullem2  33643  mdetpmtr12  33838  madjusmdetlem1  33840  pstmval  33908  sseqval  34401  cvmlift2lem6  35352  cvmlift2lem7  35353  cvmlift2lem12  35358  matunitlindflem1  37664  dvhfvadd  41138  fmpocos  42275  2arymaptfo  48694  rrxlinesc  48775  isofval2  49072  oppc1stf  49328  oppc2ndf  49329  tposcurf1  49339  diag1  49344  precofvalALT  49408