Theorem mpoeq3dva 7330

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 1118	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2749	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 578	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7319	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7260	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7260	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2804	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {coprab 7256   ∈ cmpo 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  mpoeq3ia  7331  mpoeq3dv  7332  fmpoco  7906  mapxpen  8879  cantnffval  9351  cantnfres  9365  sadfval  16087  smufval  16112  vdwapfval  16600  comfeq  17332  monpropd  17366  cofuval2  17518  cofuass  17520  cofulid  17521  cofurid  17522  catcisolem  17741  prfval  17832  prf1st  17837  prf2nd  17838  1st2ndprf  17839  xpcpropd  17842  curf1  17859  curfuncf  17872  curf2ndf  17881  grpsubpropd2  18596  mulgpropd  18660  oppglsm  19162  subglsm  19194  lsmpropd  19198  gsumcom2  19491  gsumdixp  19763  psrvscafval  21069  evlslem4  21194  evlslem2  21199  psrplusgpropd  21317  mamures  21449  mpomatmul  21503  mamutpos  21515  dmatmul  21554  dmatcrng  21559  scmatscmiddistr  21565  scmatcrng  21578  1marepvmarrepid  21632  1marepvsma1  21640  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  mdetunilem6  21674  mdetunilem7  21675  mdetunilem8  21676  mdetunilem9  21677  maduval  21695  maducoeval  21696  maducoeval2  21697  madugsum  21700  madurid  21701  smadiadetglem2  21729  cramerimplem2  21741  mat2pmatghm  21787  mat2pmatmul  21788  m2cpminvid  21810  m2cpminvid2  21812  decpmatid  21827  decpmatmulsumfsupp  21830  monmatcollpw  21836  pmatcollpwscmatlem2  21847  mp2pm2mplem3  21865  mp2pm2mplem4  21866  pm2mpghm  21873  pm2mpmhmlem1  21875  ptval2  22660  cnmpt2t  22732  cnmpt22  22733  cnmptcom  22737  cnmptk2  22745  cnmpt2plusg  23147  istgp2  23150  prdstmdd  23183  cnmpt2vsca  23254  cnmpt2ds  23912  cnmpopc  23997  cnmpt2ip  24317  rrxds  24462  rrxmfval  24475  elntg2  27256  nvmfval  28907  fedgmullem2  31613  mdetpmtr12  31677  madjusmdetlem1  31679  pstmval  31747  sseqval  32255  cvmlift2lem6  33170  cvmlift2lem7  33171  cvmlift2lem12  33176  matunitlindflem1  35700  dvhfvadd  39032  funcrngcsetcALT  45445  2arymaptfo  45888  rrxlinesc  45969