Theorem mpoeq3dva 7426

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {coprab 7350   ∈ cmpo 7351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7353  df-mpo 7354

This theorem is referenced by:  mpoeq3ia  7427  mpoeq3dv  7428  fmpoco  8028  mapxpen  9060  cantnffval  9559  cantnfres  9573  sadfval  16363  smufval  16388  vdwapfval  16883  comfeq  17612  monpropd  17644  cofuval2  17794  cofuass  17796  cofulid  17797  cofurid  17798  catcisolem  18017  prfval  18105  prf1st  18110  prf2nd  18111  1st2ndprf  18112  xpcpropd  18114  curf1  18131  curfuncf  18144  curf2ndf  18153  grpsubpropd2  18925  mulgpropd  18995  oppglsm  19521  subglsm  19552  lsmpropd  19556  gsumcom2  19854  gsumdixp  20204  funcrngcsetcALT  20526  psrvscafval  21855  evlslem4  21981  evlslem2  21984  psrplusgpropd  22118  mamures  22282  mpomatmul  22331  mamutpos  22343  dmatmul  22382  dmatcrng  22387  scmatscmiddistr  22393  scmatcrng  22406  1marepvmarrepid  22460  1marepvsma1  22468  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  mdetunilem6  22502  mdetunilem7  22503  mdetunilem8  22504  mdetunilem9  22505  maduval  22523  maducoeval  22524  maducoeval2  22525  madugsum  22528  madurid  22529  smadiadetglem2  22557  cramerimplem2  22569  mat2pmatghm  22615  mat2pmatmul  22616  m2cpminvid  22638  m2cpminvid2  22640  decpmatid  22655  decpmatmulsumfsupp  22658  monmatcollpw  22664  pmatcollpwscmatlem2  22675  mp2pm2mplem3  22693  mp2pm2mplem4  22694  pm2mpghm  22701  pm2mpmhmlem1  22703  ptval2  23486  cnmpt2t  23558  cnmpt22  23559  cnmptcom  23563  cnmptk2  23571  cnmpt2plusg  23973  istgp2  23976  prdstmdd  24009  cnmpt2vsca  24080  cnmpt2ds  24730  cnmpopc  24820  cnmpt2ip  25146  rrxds  25291  rrxmfval  25304  elntg2  28930  nvmfval  30588  elrgspnlem2  33183  fedgmullem2  33597  mdetpmtr12  33792  madjusmdetlem1  33794  pstmval  33862  sseqval  34356  cvmlift2lem6  35281  cvmlift2lem7  35282  cvmlift2lem12  35287  matunitlindflem1  37596  dvhfvadd  41070  fmpocos  42207  2arymaptfo  48639  rrxlinesc  48720  isofval2  49017  oppc1stf  49273  oppc2ndf  49274  tposcurf1  49284  diag1  49289  precofvalALT  49353