Theorem mpoeq3dva 7488

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

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

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 7415  df-mpo 7416

This theorem is referenced by:  mpoeq3ia  7489  mpoeq3dv  7490  fmpoco  8083  mapxpen  9145  cantnffval  9660  cantnfres  9674  sadfval  16395  smufval  16420  vdwapfval  16906  comfeq  17652  monpropd  17686  cofuval2  17839  cofuass  17841  cofulid  17842  cofurid  17843  catcisolem  18062  prfval  18153  prf1st  18158  prf2nd  18159  1st2ndprf  18160  xpcpropd  18163  curf1  18180  curfuncf  18193  curf2ndf  18202  grpsubpropd2  18931  mulgpropd  18998  oppglsm  19512  subglsm  19543  lsmpropd  19547  gsumcom2  19845  gsumdixp  20135  psrvscafval  21515  evlslem4  21643  evlslem2  21648  psrplusgpropd  21765  mamures  21899  mpomatmul  21955  mamutpos  21967  dmatmul  22006  dmatcrng  22011  scmatscmiddistr  22017  scmatcrng  22030  1marepvmarrepid  22084  1marepvsma1  22092  mdetrsca2  22113  mdetrlin2  22116  mdetunilem5  22125  mdetunilem6  22126  mdetunilem7  22127  mdetunilem8  22128  mdetunilem9  22129  maduval  22147  maducoeval  22148  maducoeval2  22149  madugsum  22152  madurid  22153  smadiadetglem2  22181  cramerimplem2  22193  mat2pmatghm  22239  mat2pmatmul  22240  m2cpminvid  22262  m2cpminvid2  22264  decpmatid  22279  decpmatmulsumfsupp  22282  monmatcollpw  22288  pmatcollpwscmatlem2  22299  mp2pm2mplem3  22317  mp2pm2mplem4  22318  pm2mpghm  22325  pm2mpmhmlem1  22327  ptval2  23112  cnmpt2t  23184  cnmpt22  23185  cnmptcom  23189  cnmptk2  23197  cnmpt2plusg  23599  istgp2  23602  prdstmdd  23635  cnmpt2vsca  23706  cnmpt2ds  24366  cnmpopc  24451  cnmpt2ip  24772  rrxds  24917  rrxmfval  24930  elntg2  28281  nvmfval  29935  fedgmullem2  32774  mdetpmtr12  32874  madjusmdetlem1  32876  pstmval  32944  sseqval  33456  cvmlift2lem6  34368  cvmlift2lem7  34369  cvmlift2lem12  34374  matunitlindflem1  36570  dvhfvadd  40048  fmpocos  41142  funcrngcsetcALT  46976  2arymaptfo  47418  rrxlinesc  47499