Theorem mpoeq3dva 7504

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 1117	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2737	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 577	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7493	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7431	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7431	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2791	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099  {coprab 7427   ∈ cmpo 7428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-oprab 7430  df-mpo 7431

This theorem is referenced by:  mpoeq3ia  7505  mpoeq3dv  7506  fmpoco  8111  mapxpen  9183  cantnffval  9708  cantnfres  9722  sadfval  16454  smufval  16479  vdwapfval  16975  comfeq  17721  monpropd  17755  cofuval2  17908  cofuass  17910  cofulid  17911  cofurid  17912  catcisolem  18134  prfval  18225  prf1st  18230  prf2nd  18231  1st2ndprf  18232  xpcpropd  18235  curf1  18252  curfuncf  18265  curf2ndf  18274  grpsubpropd2  19042  mulgpropd  19112  oppglsm  19642  subglsm  19673  lsmpropd  19677  gsumcom2  19975  gsumdixp  20300  funcrngcsetcALT  20621  psrvscafval  21959  evlslem4  22091  evlslem2  22096  psrplusgpropd  22227  mamures  22391  mpomatmul  22442  mamutpos  22454  dmatmul  22493  dmatcrng  22498  scmatscmiddistr  22504  scmatcrng  22517  1marepvmarrepid  22571  1marepvsma1  22579  mdetrsca2  22600  mdetrlin2  22603  mdetunilem5  22612  mdetunilem6  22613  mdetunilem7  22614  mdetunilem8  22615  mdetunilem9  22616  maduval  22634  maducoeval  22635  maducoeval2  22636  madugsum  22639  madurid  22640  smadiadetglem2  22668  cramerimplem2  22680  mat2pmatghm  22726  mat2pmatmul  22727  m2cpminvid  22749  m2cpminvid2  22751  decpmatid  22766  decpmatmulsumfsupp  22769  monmatcollpw  22775  pmatcollpwscmatlem2  22786  mp2pm2mplem3  22804  mp2pm2mplem4  22805  pm2mpghm  22812  pm2mpmhmlem1  22814  ptval2  23599  cnmpt2t  23671  cnmpt22  23672  cnmptcom  23676  cnmptk2  23684  cnmpt2plusg  24086  istgp2  24089  prdstmdd  24122  cnmpt2vsca  24193  cnmpt2ds  24853  cnmpopc  24943  cnmpt2ip  25270  rrxds  25415  rrxmfval  25428  elntg2  28922  nvmfval  30580  fedgmullem2  33527  mdetpmtr12  33642  madjusmdetlem1  33644  pstmval  33712  sseqval  34224  cvmlift2lem6  35138  cvmlift2lem7  35139  cvmlift2lem12  35144  matunitlindflem1  37319  dvhfvadd  40792  fmpocos  41960  2arymaptfo  48060  rrxlinesc  48141