Theorem mpoeq3dva 7288

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 1122	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2748	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 582	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7277	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7218	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7218	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2803	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  {coprab 7214   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-oprab 7217  df-mpo 7218

This theorem is referenced by:  mpoeq3ia  7289  mpoeq3dv  7290  ofeq  7471  fmpoco  7863  mapxpen  8812  cantnffval  9278  cantnfres  9292  sadfval  16011  smufval  16036  vdwapfval  16524  comfeq  17209  monpropd  17242  cofuval2  17393  cofuass  17395  cofulid  17396  cofurid  17397  catcisolem  17616  prfval  17706  prf1st  17711  prf2nd  17712  1st2ndprf  17713  xpcpropd  17716  curf1  17733  curfuncf  17746  curf2ndf  17755  grpsubpropd2  18469  mulgpropd  18533  oppglsm  19031  subglsm  19063  lsmpropd  19067  gsumcom2  19360  gsumdixp  19627  psrvscafval  20915  evlslem4  21034  evlslem2  21039  psrplusgpropd  21157  mamures  21289  mpomatmul  21343  mamutpos  21355  dmatmul  21394  dmatcrng  21399  scmatscmiddistr  21405  scmatcrng  21418  1marepvmarrepid  21472  1marepvsma1  21480  mdetrsca2  21501  mdetrlin2  21504  mdetunilem5  21513  mdetunilem6  21514  mdetunilem7  21515  mdetunilem8  21516  mdetunilem9  21517  maduval  21535  maducoeval  21536  maducoeval2  21537  madugsum  21540  madurid  21541  smadiadetglem2  21569  cramerimplem2  21581  mat2pmatghm  21627  mat2pmatmul  21628  m2cpminvid  21650  m2cpminvid2  21652  decpmatid  21667  decpmatmulsumfsupp  21670  monmatcollpw  21676  pmatcollpwscmatlem2  21687  mp2pm2mplem3  21705  mp2pm2mplem4  21706  pm2mpghm  21713  pm2mpmhmlem1  21715  ptval2  22498  cnmpt2t  22570  cnmpt22  22571  cnmptcom  22575  cnmptk2  22583  cnmpt2plusg  22985  istgp2  22988  prdstmdd  23021  cnmpt2vsca  23092  cnmpt2ds  23740  cnmpopc  23825  cnmpt2ip  24145  rrxds  24290  rrxmfval  24303  elntg2  27076  nvmfval  28725  fedgmullem2  31425  mdetpmtr12  31489  madjusmdetlem1  31491  pstmval  31559  sseqval  32067  cvmlift2lem6  32983  cvmlift2lem7  32984  cvmlift2lem12  32989  matunitlindflem1  35510  dvhfvadd  38842  funcrngcsetcALT  45230  2arymaptfo  45673  rrxlinesc  45754