Theorem mpoeq3dva 7528

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {coprab 7452   ∈ cmpo 7453

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-oprab 7455  df-mpo 7456

This theorem is used by:  mpoeq3ia  7529  mpoeq3dv  7530  fmpoco  8142  mapxpen  9200  cantnffval  9701  cantnfres  9715  sadfval  16666  smufval  16691  vdwapfval  17193  comfeq  17930  monpropd  17962  cofuval2  18112  cofuass  18114  cofulid  18115  cofurid  18116  catcisolem  18335  prfval  18423  prf1st  18428  prf2nd  18429  1st2ndprf  18430  xpcpropd  18432  curf1  18449  curfuncf  18462  curf2ndf  18471  grpsubpropd2  19306  mulgpropd  19376  oppglsm  19907  subglsm  19938  lsmpropd  19942  gsumcom2  20240  gsumdixp  20599  funcrngcsetcALT  20944  psrvscafval  22311  evlslem4  22440  evlslem2  22443  psrplusgpropd  22608  mamures  22767  mpomatmul  22816  mamutpos  22828  dmatmul  22867  dmatcrng  22872  scmatscmiddistr  22878  scmatcrng  22891  1marepvmarrepid  22945  1marepvsma1  22953  mdetrsca2  22974  mdetrlin2  22977  mdetunilem5  22986  mdetunilem6  22987  mdetunilem7  22988  mdetunilem8  22989  mdetunilem9  22990  maduval  23008  maducoeval  23009  maducoeval2  23010  madugsum  23013  madurid  23014  smadiadetglem2  23042  matunitlindflem1  23049  cramerimplem2  23057  mat2pmatghm  23103  mat2pmatmul  23104  m2cpminvid  23126  m2cpminvid2  23128  decpmatid  23143  decpmatmulsumfsupp  23146  monmatcollpw  23152  pmatcollpwscmatlem2  23163  mp2pm2mplem3  23181  mp2pm2mplem4  23182  pm2mpghm  23189  pm2mpmhmlem1  23191  ptval2  23975  cnmpt2t  24047  cnmpt22  24048  cnmptcom  24052  cnmptk2  24060  cnmpt2plusg  24462  istgp2  24465  prdstmdd  24498  cnmpt2vsca  24569  cnmpt2ds  25218  cnmpopc  25304  cnmpt2ip  25624  rrxds  25769  rrxmfval  25782  elntg2  29620  nvmfval  31303  elrgspnlem2  33903  fedgmullem2  34373  mdetpmtr12  34568  madjusmdetlem1  34570  pstmval  34638  sseqval  35131  cvmlift2lem6  36281  cvmlift2lem7  36282  cvmlift2lem12  36287  dvhfvadd  42414  fmpocos  43554  2arymaptfo  50097  rrxlinesc  50179  isofval2  50477  oppc1stf  50741  oppc2ndf  50742  tposcurf1  50752  diag1  50757  precofvalALT  50834