Theorem mpoeq3dva 7433

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 1126	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2750	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 584	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7422	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7361	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7361	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2799	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  {coprab 7357   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  mpoeq3ia  7434  mpoeq3dv  7435  fmpoco  8034  mapxpen  9071  cantnffval  9575  cantnfres  9589  sadfval  16412  smufval  16437  vdwapfval  16933  comfeq  17663  monpropd  17695  cofuval2  17845  cofuass  17847  cofulid  17848  cofurid  17849  catcisolem  18068  prfval  18156  prf1st  18161  prf2nd  18162  1st2ndprf  18163  xpcpropd  18165  curf1  18182  curfuncf  18195  curf2ndf  18204  grpsubpropd2  19013  mulgpropd  19083  oppglsm  19608  subglsm  19639  lsmpropd  19643  gsumcom2  19941  gsumdixp  20289  funcrngcsetcALT  20613  psrvscafval  21923  evlslem4  22052  evlslem2  22055  psrplusgpropd  22220  mamures  22380  mpomatmul  22429  mamutpos  22441  dmatmul  22480  dmatcrng  22485  scmatscmiddistr  22491  scmatcrng  22504  1marepvmarrepid  22558  1marepvsma1  22566  mdetrsca2  22587  mdetrlin2  22590  mdetunilem5  22599  mdetunilem6  22600  mdetunilem7  22601  mdetunilem8  22602  mdetunilem9  22603  maduval  22621  maducoeval  22622  maducoeval2  22623  madugsum  22626  madurid  22627  smadiadetglem2  22655  cramerimplem2  22667  mat2pmatghm  22713  mat2pmatmul  22714  m2cpminvid  22736  m2cpminvid2  22738  decpmatid  22753  decpmatmulsumfsupp  22756  monmatcollpw  22762  pmatcollpwscmatlem2  22773  mp2pm2mplem3  22791  mp2pm2mplem4  22792  pm2mpghm  22799  pm2mpmhmlem1  22801  ptval2  23584  cnmpt2t  23656  cnmpt22  23657  cnmptcom  23661  cnmptk2  23669  cnmpt2plusg  24071  istgp2  24074  prdstmdd  24107  cnmpt2vsca  24178  cnmpt2ds  24827  cnmpopc  24913  cnmpt2ip  25233  rrxds  25378  rrxmfval  25391  elntg2  29072  nvmfval  30733  elrgspnlem2  33324  fedgmullem2  33814  mdetpmtr12  34009  madjusmdetlem1  34011  pstmval  34079  sseqval  34572  cvmlift2lem6  35536  cvmlift2lem7  35537  cvmlift2lem12  35542  matunitlindflem1  37983  dvhfvadd  41583  fmpocos  42720  2arymaptfo  49145  rrxlinesc  49226  isofval2  49522  oppc1stf  49778  oppc2ndf  49779  tposcurf1  49789  diag1  49794  precofvalALT  49858