Theorem mpoeq3dva 7491

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {coprab 7415   ∈ cmpo 7416

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 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-oprab 7418  df-mpo 7419

This theorem is used by:  mpoeq3ia  7492  mpoeq3dv  7493  fmpoco  8093  mapxpen  9142  cantnffval  9643  cantnfres  9657  sadfval  16543  smufval  16568  vdwapfval  17064  comfeq  17795  monpropd  17827  cofuval2  17977  cofuass  17979  cofulid  17980  cofurid  17981  catcisolem  18200  prfval  18288  prf1st  18293  prf2nd  18294  1st2ndprf  18295  xpcpropd  18297  curf1  18314  curfuncf  18327  curf2ndf  18336  grpsubpropd2  19170  mulgpropd  19240  oppglsm  19770  subglsm  19801  lsmpropd  19805  gsumcom2  20103  gsumdixp  20460  funcrngcsetcALT  20804  psrvscafval  22164  evlslem4  22293  evlslem2  22296  psrplusgpropd  22461  mamures  22620  mpomatmul  22669  mamutpos  22681  dmatmul  22720  dmatcrng  22725  scmatscmiddistr  22731  scmatcrng  22744  1marepvmarrepid  22798  1marepvsma1  22806  mdetrsca2  22827  mdetrlin2  22830  mdetunilem5  22839  mdetunilem6  22840  mdetunilem7  22841  mdetunilem8  22842  mdetunilem9  22843  maduval  22861  maducoeval  22862  maducoeval2  22863  madugsum  22866  madurid  22867  smadiadetglem2  22895  matunitlindflem1  22902  cramerimplem2  22910  mat2pmatghm  22956  mat2pmatmul  22957  m2cpminvid  22979  m2cpminvid2  22981  decpmatid  22996  decpmatmulsumfsupp  22999  monmatcollpw  23005  pmatcollpwscmatlem2  23016  mp2pm2mplem3  23034  mp2pm2mplem4  23035  pm2mpghm  23042  pm2mpmhmlem1  23044  ptval2  23828  cnmpt2t  23900  cnmpt22  23901  cnmptcom  23905  cnmptk2  23913  cnmpt2plusg  24315  istgp2  24318  prdstmdd  24351  cnmpt2vsca  24422  cnmpt2ds  25071  cnmpopc  25157  cnmpt2ip  25477  rrxds  25622  rrxmfval  25635  elntg2  29443  nvmfval  31126  elrgspnlem2  33684  fedgmullem2  34141  mdetpmtr12  34336  madjusmdetlem1  34338  pstmval  34406  sseqval  34900  cvmlift2lem6  35888  cvmlift2lem7  35889  cvmlift2lem12  35894  dvhfvadd  41965  fmpocos  43104  2arymaptfo  49585  rrxlinesc  49666  isofval2  49959  oppc1stf  50215  oppc2ndf  50216  tposcurf1  50226  diag1  50231  precofvalALT  50295