Theorem mpoeq3dva 7444

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  mpoeq3ia  7445  mpoeq3dv  7446  fmpoco  8045  mapxpen  9081  cantnffval  9584  cantnfres  9598  sadfval  16421  smufval  16446  vdwapfval  16942  comfeq  17672  monpropd  17704  cofuval2  17854  cofuass  17856  cofulid  17857  cofurid  17858  catcisolem  18077  prfval  18165  prf1st  18170  prf2nd  18171  1st2ndprf  18172  xpcpropd  18174  curf1  18191  curfuncf  18204  curf2ndf  18213  grpsubpropd2  19022  mulgpropd  19092  oppglsm  19617  subglsm  19648  lsmpropd  19652  gsumcom2  19950  gsumdixp  20298  funcrngcsetcALT  20618  psrvscafval  21927  evlslem4  22054  evlslem2  22057  psrplusgpropd  22199  mamures  22362  mpomatmul  22411  mamutpos  22423  dmatmul  22462  dmatcrng  22467  scmatscmiddistr  22473  scmatcrng  22486  1marepvmarrepid  22540  1marepvsma1  22548  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  mdetunilem6  22582  mdetunilem7  22583  mdetunilem8  22584  mdetunilem9  22585  maduval  22603  maducoeval  22604  maducoeval2  22605  madugsum  22608  madurid  22609  smadiadetglem2  22637  cramerimplem2  22649  mat2pmatghm  22695  mat2pmatmul  22696  m2cpminvid  22718  m2cpminvid2  22720  decpmatid  22735  decpmatmulsumfsupp  22738  monmatcollpw  22744  pmatcollpwscmatlem2  22755  mp2pm2mplem3  22773  mp2pm2mplem4  22774  pm2mpghm  22781  pm2mpmhmlem1  22783  ptval2  23566  cnmpt2t  23638  cnmpt22  23639  cnmptcom  23643  cnmptk2  23651  cnmpt2plusg  24053  istgp2  24056  prdstmdd  24089  cnmpt2vsca  24160  cnmpt2ds  24809  cnmpopc  24895  cnmpt2ip  25215  rrxds  25360  rrxmfval  25373  elntg2  29054  nvmfval  30715  elrgspnlem2  33304  fedgmullem2  33774  mdetpmtr12  33969  madjusmdetlem1  33971  pstmval  34039  sseqval  34532  cvmlift2lem6  35490  cvmlift2lem7  35491  cvmlift2lem12  35496  matunitlindflem1  37937  dvhfvadd  41537  fmpocos  42675  2arymaptfo  49130  rrxlinesc  49211  isofval2  49507  oppc1stf  49763  oppc2ndf  49764  tposcurf1  49774  diag1  49779  precofvalALT  49843