Theorem mpoeq3dva 7477

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  {coprab 7401   ∈ cmpo 7402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-oprab 7404  df-mpo 7405

This theorem is referenced by:  mpoeq3ia  7478  mpoeq3dv  7479  fmpoco  8078  mapxpen  9119  cantnffval  9620  cantnfres  9634  sadfval  16498  smufval  16523  vdwapfval  17019  comfeq  17750  monpropd  17782  cofuval2  17932  cofuass  17934  cofulid  17935  cofurid  17936  catcisolem  18155  prfval  18243  prf1st  18248  prf2nd  18249  1st2ndprf  18250  xpcpropd  18252  curf1  18269  curfuncf  18282  curf2ndf  18291  grpsubpropd2  19100  mulgpropd  19170  oppglsm  19700  subglsm  19731  lsmpropd  19735  gsumcom2  20033  gsumdixp  20388  funcrngcsetcALT  20714  psrvscafval  22055  evlslem4  22184  evlslem2  22187  psrplusgpropd  22352  mamures  22511  mpomatmul  22560  mamutpos  22572  dmatmul  22611  dmatcrng  22616  scmatscmiddistr  22622  scmatcrng  22635  1marepvmarrepid  22689  1marepvsma1  22697  mdetrsca2  22718  mdetrlin2  22721  mdetunilem5  22730  mdetunilem6  22731  mdetunilem7  22732  mdetunilem8  22733  mdetunilem9  22734  maduval  22752  maducoeval  22753  maducoeval2  22754  madugsum  22757  madurid  22758  smadiadetglem2  22786  cramerimplem2  22798  mat2pmatghm  22844  mat2pmatmul  22845  m2cpminvid  22867  m2cpminvid2  22869  decpmatid  22884  decpmatmulsumfsupp  22887  monmatcollpw  22893  pmatcollpwscmatlem2  22904  mp2pm2mplem3  22922  mp2pm2mplem4  22923  pm2mpghm  22930  pm2mpmhmlem1  22932  ptval2  23715  cnmpt2t  23787  cnmpt22  23788  cnmptcom  23792  cnmptk2  23800  cnmpt2plusg  24202  istgp2  24205  prdstmdd  24238  cnmpt2vsca  24309  cnmpt2ds  24958  cnmpopc  25044  cnmpt2ip  25364  rrxds  25509  rrxmfval  25522  elntg2  29240  nvmfval  30901  elrgspnlem2  33471  fedgmullem2  33932  mdetpmtr12  34127  madjusmdetlem1  34129  pstmval  34197  sseqval  34690  cvmlift2lem6  35666  cvmlift2lem7  35667  cvmlift2lem12  35672  matunitlindflem1  38122  dvhfvadd  41722  fmpocos  42859  2arymaptfo  49286  rrxlinesc  49367  isofval2  49662  oppc1stf  49918  oppc2ndf  49919  tposcurf1  49929  diag1  49934  precofvalALT  49998