Theorem mpoeq3dva 7510

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  {coprab 7432   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  mpoeq3ia  7511  mpoeq3dv  7512  fmpoco  8119  mapxpen  9182  cantnffval  9701  cantnfres  9715  sadfval  16486  smufval  16511  vdwapfval  17005  comfeq  17751  monpropd  17785  cofuval2  17938  cofuass  17940  cofulid  17941  cofurid  17942  catcisolem  18164  prfval  18255  prf1st  18260  prf2nd  18261  1st2ndprf  18262  xpcpropd  18265  curf1  18282  curfuncf  18295  curf2ndf  18304  grpsubpropd2  19077  mulgpropd  19147  oppglsm  19675  subglsm  19706  lsmpropd  19710  gsumcom2  20008  gsumdixp  20333  funcrngcsetcALT  20658  psrvscafval  21986  evlslem4  22118  evlslem2  22121  psrplusgpropd  22253  mamures  22417  mpomatmul  22468  mamutpos  22480  dmatmul  22519  dmatcrng  22524  scmatscmiddistr  22530  scmatcrng  22543  1marepvmarrepid  22597  1marepvsma1  22605  mdetrsca2  22626  mdetrlin2  22629  mdetunilem5  22638  mdetunilem6  22639  mdetunilem7  22640  mdetunilem8  22641  mdetunilem9  22642  maduval  22660  maducoeval  22661  maducoeval2  22662  madugsum  22665  madurid  22666  smadiadetglem2  22694  cramerimplem2  22706  mat2pmatghm  22752  mat2pmatmul  22753  m2cpminvid  22775  m2cpminvid2  22777  decpmatid  22792  decpmatmulsumfsupp  22795  monmatcollpw  22801  pmatcollpwscmatlem2  22812  mp2pm2mplem3  22830  mp2pm2mplem4  22831  pm2mpghm  22838  pm2mpmhmlem1  22840  ptval2  23625  cnmpt2t  23697  cnmpt22  23698  cnmptcom  23702  cnmptk2  23710  cnmpt2plusg  24112  istgp2  24115  prdstmdd  24148  cnmpt2vsca  24219  cnmpt2ds  24879  cnmpopc  24969  cnmpt2ip  25296  rrxds  25441  rrxmfval  25454  elntg2  29015  nvmfval  30673  elrgspnlem2  33233  fedgmullem2  33658  mdetpmtr12  33786  madjusmdetlem1  33788  pstmval  33856  sseqval  34370  cvmlift2lem6  35293  cvmlift2lem7  35294  cvmlift2lem12  35299  matunitlindflem1  37603  dvhfvadd  41074  fmpocos  42254  2arymaptfo  48504  rrxlinesc  48585