Theorem mpoeq3dva 7445

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {coprab 7369   ∈ cmpo 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  mpoeq3ia  7446  mpoeq3dv  7447  fmpoco  8047  mapxpen  9083  cantnffval  9584  cantnfres  9598  sadfval  16391  smufval  16416  vdwapfval  16911  comfeq  17641  monpropd  17673  cofuval2  17823  cofuass  17825  cofulid  17826  cofurid  17827  catcisolem  18046  prfval  18134  prf1st  18139  prf2nd  18140  1st2ndprf  18141  xpcpropd  18143  curf1  18160  curfuncf  18173  curf2ndf  18182  grpsubpropd2  18988  mulgpropd  19058  oppglsm  19583  subglsm  19614  lsmpropd  19618  gsumcom2  19916  gsumdixp  20266  funcrngcsetcALT  20586  psrvscafval  21916  evlslem4  22043  evlslem2  22046  psrplusgpropd  22188  mamures  22353  mpomatmul  22402  mamutpos  22414  dmatmul  22453  dmatcrng  22458  scmatscmiddistr  22464  scmatcrng  22477  1marepvmarrepid  22531  1marepvsma1  22539  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  mdetunilem6  22573  mdetunilem7  22574  mdetunilem8  22575  mdetunilem9  22576  maduval  22594  maducoeval  22595  maducoeval2  22596  madugsum  22599  madurid  22600  smadiadetglem2  22628  cramerimplem2  22640  mat2pmatghm  22686  mat2pmatmul  22687  m2cpminvid  22709  m2cpminvid2  22711  decpmatid  22726  decpmatmulsumfsupp  22729  monmatcollpw  22735  pmatcollpwscmatlem2  22746  mp2pm2mplem3  22764  mp2pm2mplem4  22765  pm2mpghm  22772  pm2mpmhmlem1  22774  ptval2  23557  cnmpt2t  23629  cnmpt22  23630  cnmptcom  23634  cnmptk2  23642  cnmpt2plusg  24044  istgp2  24047  prdstmdd  24080  cnmpt2vsca  24151  cnmpt2ds  24800  cnmpopc  24890  cnmpt2ip  25216  rrxds  25361  rrxmfval  25374  elntg2  29070  nvmfval  30732  elrgspnlem2  33337  fedgmullem2  33808  mdetpmtr12  34003  madjusmdetlem1  34005  pstmval  34073  sseqval  34566  cvmlift2lem6  35524  cvmlift2lem7  35525  cvmlift2lem12  35530  matunitlindflem1  37867  dvhfvadd  41467  fmpocos  42606  2arymaptfo  49014  rrxlinesc  49095  isofval2  49391  oppc1stf  49647  oppc2ndf  49648  tposcurf1  49658  diag1  49663  precofvalALT  49727