Theorem mpoeq3dva 7438

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 7427	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7366	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7366	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2797	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

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

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 7365  df-mpo 7366

This theorem is referenced by:  mpoeq3ia  7439  mpoeq3dv  7440  fmpoco  8039  mapxpen  9075  cantnffval  9578  cantnfres  9592  sadfval  16415  smufval  16440  vdwapfval  16936  comfeq  17666  monpropd  17698  cofuval2  17848  cofuass  17850  cofulid  17851  cofurid  17852  catcisolem  18071  prfval  18159  prf1st  18164  prf2nd  18165  1st2ndprf  18166  xpcpropd  18168  curf1  18185  curfuncf  18198  curf2ndf  18207  grpsubpropd2  19016  mulgpropd  19086  oppglsm  19611  subglsm  19642  lsmpropd  19646  gsumcom2  19944  gsumdixp  20292  funcrngcsetcALT  20612  psrvscafval  21940  evlslem4  22067  evlslem2  22070  psrplusgpropd  22212  mamures  22375  mpomatmul  22424  mamutpos  22436  dmatmul  22475  dmatcrng  22480  scmatscmiddistr  22486  scmatcrng  22499  1marepvmarrepid  22553  1marepvsma1  22561  mdetrsca2  22582  mdetrlin2  22585  mdetunilem5  22594  mdetunilem6  22595  mdetunilem7  22596  mdetunilem8  22597  mdetunilem9  22598  maduval  22616  maducoeval  22617  maducoeval2  22618  madugsum  22621  madurid  22622  smadiadetglem2  22650  cramerimplem2  22662  mat2pmatghm  22708  mat2pmatmul  22709  m2cpminvid  22731  m2cpminvid2  22733  decpmatid  22748  decpmatmulsumfsupp  22751  monmatcollpw  22757  pmatcollpwscmatlem2  22768  mp2pm2mplem3  22786  mp2pm2mplem4  22787  pm2mpghm  22794  pm2mpmhmlem1  22796  ptval2  23579  cnmpt2t  23651  cnmpt22  23652  cnmptcom  23656  cnmptk2  23664  cnmpt2plusg  24066  istgp2  24069  prdstmdd  24102  cnmpt2vsca  24173  cnmpt2ds  24822  cnmpopc  24908  cnmpt2ip  25228  rrxds  25373  rrxmfval  25386  elntg2  29071  nvmfval  30733  elrgspnlem2  33322  fedgmullem2  33793  mdetpmtr12  33988  madjusmdetlem1  33990  pstmval  34058  sseqval  34551  cvmlift2lem6  35509  cvmlift2lem7  35510  cvmlift2lem12  35515  matunitlindflem1  37954  dvhfvadd  41554  fmpocos  42692  2arymaptfo  49145  rrxlinesc  49226  isofval2  49522  oppc1stf  49778  oppc2ndf  49779  tposcurf1  49789  diag1  49794  precofvalALT  49858