Theorem mpoeq3dva 7433

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 2745	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 579	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7422	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7361	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7361	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2794	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  {coprab 7357   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  mpoeq3ia  7434  mpoeq3dv  7435  fmpoco  8035  mapxpen  9069  cantnffval  9570  cantnfres  9584  sadfval  16377  smufval  16402  vdwapfval  16897  comfeq  17627  monpropd  17659  cofuval2  17809  cofuass  17811  cofulid  17812  cofurid  17813  catcisolem  18032  prfval  18120  prf1st  18125  prf2nd  18126  1st2ndprf  18127  xpcpropd  18129  curf1  18146  curfuncf  18159  curf2ndf  18168  grpsubpropd2  18974  mulgpropd  19044  oppglsm  19569  subglsm  19600  lsmpropd  19604  gsumcom2  19902  gsumdixp  20252  funcrngcsetcALT  20572  psrvscafval  21902  evlslem4  22029  evlslem2  22032  psrplusgpropd  22174  mamures  22339  mpomatmul  22388  mamutpos  22400  dmatmul  22439  dmatcrng  22444  scmatscmiddistr  22450  scmatcrng  22463  1marepvmarrepid  22517  1marepvsma1  22525  mdetrsca2  22546  mdetrlin2  22549  mdetunilem5  22558  mdetunilem6  22559  mdetunilem7  22560  mdetunilem8  22561  mdetunilem9  22562  maduval  22580  maducoeval  22581  maducoeval2  22582  madugsum  22585  madurid  22586  smadiadetglem2  22614  cramerimplem2  22626  mat2pmatghm  22672  mat2pmatmul  22673  m2cpminvid  22695  m2cpminvid2  22697  decpmatid  22712  decpmatmulsumfsupp  22715  monmatcollpw  22721  pmatcollpwscmatlem2  22732  mp2pm2mplem3  22750  mp2pm2mplem4  22751  pm2mpghm  22758  pm2mpmhmlem1  22760  ptval2  23543  cnmpt2t  23615  cnmpt22  23616  cnmptcom  23620  cnmptk2  23628  cnmpt2plusg  24030  istgp2  24033  prdstmdd  24066  cnmpt2vsca  24137  cnmpt2ds  24786  cnmpopc  24876  cnmpt2ip  25202  rrxds  25347  rrxmfval  25360  elntg2  29007  nvmfval  30668  elrgspnlem2  33274  fedgmullem2  33736  mdetpmtr12  33931  madjusmdetlem1  33933  pstmval  34001  sseqval  34494  cvmlift2lem6  35451  cvmlift2lem7  35452  cvmlift2lem12  35457  matunitlindflem1  37756  dvhfvadd  41290  fmpocos  42432  2arymaptfo  48842  rrxlinesc  48923  isofval2  49219  oppc1stf  49475  oppc2ndf  49476  tposcurf1  49486  diag1  49491  precofvalALT  49555