Theorem mpoeq3dva 7482

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {coprab 7406   ∈ cmpo 7407

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  mpoeq3ia  7483  mpoeq3dv  7484  fmpoco  8077  mapxpen  9139  cantnffval  9654  cantnfres  9668  sadfval  16389  smufval  16414  vdwapfval  16900  comfeq  17646  monpropd  17680  cofuval2  17833  cofuass  17835  cofulid  17836  cofurid  17837  catcisolem  18056  prfval  18147  prf1st  18152  prf2nd  18153  1st2ndprf  18154  xpcpropd  18157  curf1  18174  curfuncf  18187  curf2ndf  18196  grpsubpropd2  18925  mulgpropd  18990  oppglsm  19504  subglsm  19535  lsmpropd  19539  gsumcom2  19837  gsumdixp  20124  psrvscafval  21500  evlslem4  21628  evlslem2  21633  psrplusgpropd  21749  mamures  21883  mpomatmul  21939  mamutpos  21951  dmatmul  21990  dmatcrng  21995  scmatscmiddistr  22001  scmatcrng  22014  1marepvmarrepid  22068  1marepvsma1  22076  mdetrsca2  22097  mdetrlin2  22100  mdetunilem5  22109  mdetunilem6  22110  mdetunilem7  22111  mdetunilem8  22112  mdetunilem9  22113  maduval  22131  maducoeval  22132  maducoeval2  22133  madugsum  22136  madurid  22137  smadiadetglem2  22165  cramerimplem2  22177  mat2pmatghm  22223  mat2pmatmul  22224  m2cpminvid  22246  m2cpminvid2  22248  decpmatid  22263  decpmatmulsumfsupp  22266  monmatcollpw  22272  pmatcollpwscmatlem2  22283  mp2pm2mplem3  22301  mp2pm2mplem4  22302  pm2mpghm  22309  pm2mpmhmlem1  22311  ptval2  23096  cnmpt2t  23168  cnmpt22  23169  cnmptcom  23173  cnmptk2  23181  cnmpt2plusg  23583  istgp2  23586  prdstmdd  23619  cnmpt2vsca  23690  cnmpt2ds  24350  cnmpopc  24435  cnmpt2ip  24756  rrxds  24901  rrxmfval  24914  elntg2  28232  nvmfval  29884  fedgmullem2  32703  mdetpmtr12  32793  madjusmdetlem1  32795  pstmval  32863  sseqval  33375  cvmlift2lem6  34287  cvmlift2lem7  34288  cvmlift2lem12  34293  matunitlindflem1  36472  dvhfvadd  39950  fmpocos  41053  funcrngcsetcALT  46850  2arymaptfo  47293  rrxlinesc  47374