Theorem mpoeq3dva 7497

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 1138	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2772	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 590	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7486	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7425	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7425	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2821	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {coprab 7421   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-oprab 7424  df-mpo 7425

This theorem is used by:  mpoeq3ia  7498  mpoeq3dv  7499  fmpoco  8106  mapxpen  9162  cantnffval  9664  cantnfres  9678  sadfval  16622  smufval  16647  vdwapfval  17149  comfeq  17880  monpropd  17912  cofuval2  18062  cofuass  18064  cofulid  18065  cofurid  18066  catcisolem  18285  prfval  18373  prf1st  18378  prf2nd  18379  1st2ndprf  18380  xpcpropd  18382  curf1  18399  curfuncf  18412  curf2ndf  18421  grpsubpropd2  19256  mulgpropd  19326  oppglsm  19856  subglsm  19887  lsmpropd  19891  gsumcom2  20189  gsumdixp  20548  funcrngcsetcALT  20893  psrvscafval  22256  evlslem4  22385  evlslem2  22388  psrplusgpropd  22553  mamures  22712  mpomatmul  22761  mamutpos  22773  dmatmul  22812  dmatcrng  22817  scmatscmiddistr  22823  scmatcrng  22836  1marepvmarrepid  22890  1marepvsma1  22898  mdetrsca2  22919  mdetrlin2  22922  mdetunilem5  22931  mdetunilem6  22932  mdetunilem7  22933  mdetunilem8  22934  mdetunilem9  22935  maduval  22953  maducoeval  22954  maducoeval2  22955  madugsum  22958  madurid  22959  smadiadetglem2  22987  matunitlindflem1  22994  cramerimplem2  23002  mat2pmatghm  23048  mat2pmatmul  23049  m2cpminvid  23071  m2cpminvid2  23073  decpmatid  23088  decpmatmulsumfsupp  23091  monmatcollpw  23097  pmatcollpwscmatlem2  23108  mp2pm2mplem3  23126  mp2pm2mplem4  23127  pm2mpghm  23134  pm2mpmhmlem1  23136  ptval2  23920  cnmpt2t  23992  cnmpt22  23993  cnmptcom  23997  cnmptk2  24005  cnmpt2plusg  24407  istgp2  24410  prdstmdd  24443  cnmpt2vsca  24514  cnmpt2ds  25163  cnmpopc  25249  cnmpt2ip  25569  rrxds  25714  rrxmfval  25727  elntg2  29563  nvmfval  31246  elrgspnlem2  33804  fedgmullem2  34262  mdetpmtr12  34457  madjusmdetlem1  34459  pstmval  34527  sseqval  35020  cvmlift2lem6  36073  cvmlift2lem7  36074  cvmlift2lem12  36079  dvhfvadd  42148  fmpocos  43287  2arymaptfo  49765  rrxlinesc  49846  isofval2  50139  oppc1stf  50395  oppc2ndf  50396  tposcurf1  50406  diag1  50411  precofvalALT  50475