Theorem mpoeq3dva 7089

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  {coprab 7017   ∈ cmpo 7018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-oprab 7020  df-mpo 7021

This theorem is referenced by:  mpoeq3ia  7090  mpoeq3dv  7091  ofeq  7269  fmpoco  7646  mapxpen  8530  cantnffval  8972  cantnfres  8986  sadfval  15634  smufval  15659  vdwapfval  16136  comfeq  16805  monpropd  16836  cofuval2  16986  cofuass  16988  cofulid  16989  cofurid  16990  catcisolem  17195  prfval  17278  prf1st  17283  prf2nd  17284  1st2ndprf  17285  xpcpropd  17287  curf1  17304  curfuncf  17317  curf2ndf  17326  grpsubpropd2  17962  mulgpropd  18023  oppglsm  18497  subglsm  18526  lsmpropd  18530  gsumcom2  18815  gsumdixp  19049  psrvscafval  19858  evlslem4  19975  evlslem2  19979  psrplusgpropd  20087  mamures  20683  mpomatmul  20739  mamutpos  20751  dmatmul  20790  dmatcrng  20795  scmatscmiddistr  20801  scmatcrng  20814  1marepvmarrepid  20868  1marepvsma1  20876  mdetrsca2  20897  mdetrlin2  20900  mdetunilem5  20909  mdetunilem6  20910  mdetunilem7  20911  mdetunilem8  20912  mdetunilem9  20913  maduval  20931  maducoeval  20932  maducoeval2  20933  madugsum  20936  madurid  20937  smadiadetglem2  20965  cramerimplem2  20977  mat2pmatghm  21022  mat2pmatmul  21023  m2cpminvid  21045  m2cpminvid2  21047  decpmatid  21062  decpmatmulsumfsupp  21065  monmatcollpw  21071  pmatcollpwscmatlem2  21082  mp2pm2mplem3  21100  mp2pm2mplem4  21101  pm2mpghm  21108  pm2mpmhmlem1  21110  ptval2  21893  cnmpt2t  21965  cnmpt22  21966  cnmptcom  21970  cnmptk2  21978  cnmpt2plusg  22380  istgp2  22383  prdstmdd  22415  cnmpt2vsca  22486  cnmpt2ds  23134  cnmpopc  23215  cnmpt2ip  23534  rrxds  23679  rrxmfval  23692  elntg2  26454  nvmfval  28112  fedgmullem2  30630  mdetpmtr12  30705  madjusmdetlem1  30707  pstmval  30752  sseqval  31263  cvmlift2lem6  32164  cvmlift2lem7  32165  cvmlift2lem12  32170  matunitlindflem1  34438  dvhfvadd  37777  funcrngcsetcALT  43768  rrxlinesc  44223