Theorem mpoeq3dva 7435

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  {coprab 7359   ∈ cmpo 7360

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 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  mpoeq3ia  7436  mpoeq3dv  7437  fmpoco  8037  mapxpen  9071  cantnffval  9572  cantnfres  9586  sadfval  16379  smufval  16404  vdwapfval  16899  comfeq  17629  monpropd  17661  cofuval2  17811  cofuass  17813  cofulid  17814  cofurid  17815  catcisolem  18034  prfval  18122  prf1st  18127  prf2nd  18128  1st2ndprf  18129  xpcpropd  18131  curf1  18148  curfuncf  18161  curf2ndf  18170  grpsubpropd2  18976  mulgpropd  19046  oppglsm  19571  subglsm  19602  lsmpropd  19606  gsumcom2  19904  gsumdixp  20254  funcrngcsetcALT  20574  psrvscafval  21904  evlslem4  22031  evlslem2  22034  psrplusgpropd  22176  mamures  22341  mpomatmul  22390  mamutpos  22402  dmatmul  22441  dmatcrng  22446  scmatscmiddistr  22452  scmatcrng  22465  1marepvmarrepid  22519  1marepvsma1  22527  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  mdetunilem6  22561  mdetunilem7  22562  mdetunilem8  22563  mdetunilem9  22564  maduval  22582  maducoeval  22583  maducoeval2  22584  madugsum  22587  madurid  22588  smadiadetglem2  22616  cramerimplem2  22628  mat2pmatghm  22674  mat2pmatmul  22675  m2cpminvid  22697  m2cpminvid2  22699  decpmatid  22714  decpmatmulsumfsupp  22717  monmatcollpw  22723  pmatcollpwscmatlem2  22734  mp2pm2mplem3  22752  mp2pm2mplem4  22753  pm2mpghm  22760  pm2mpmhmlem1  22762  ptval2  23545  cnmpt2t  23617  cnmpt22  23618  cnmptcom  23622  cnmptk2  23630  cnmpt2plusg  24032  istgp2  24035  prdstmdd  24068  cnmpt2vsca  24139  cnmpt2ds  24788  cnmpopc  24878  cnmpt2ip  25204  rrxds  25349  rrxmfval  25362  elntg2  29058  nvmfval  30719  elrgspnlem2  33325  fedgmullem2  33787  mdetpmtr12  33982  madjusmdetlem1  33984  pstmval  34052  sseqval  34545  cvmlift2lem6  35502  cvmlift2lem7  35503  cvmlift2lem12  35508  matunitlindflem1  37817  dvhfvadd  41351  fmpocos  42490  2arymaptfo  48900  rrxlinesc  48981  isofval2  49277  oppc1stf  49533  oppc2ndf  49534  tposcurf1  49544  diag1  49549  precofvalALT  49613