Theorem mpoeq3dva 7487

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 1138	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2774	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 589	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7476	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7415	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7415	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2823	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  {coprab 7411   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  mpoeq3ia  7488  mpoeq3dv  7489  fmpoco  8086  mapxpen  9127  cantnffval  9628  cantnfres  9642  sadfval  16505  smufval  16530  vdwapfval  17026  comfeq  17757  monpropd  17789  cofuval2  17939  cofuass  17941  cofulid  17942  cofurid  17943  catcisolem  18162  prfval  18250  prf1st  18255  prf2nd  18256  1st2ndprf  18257  xpcpropd  18259  curf1  18276  curfuncf  18289  curf2ndf  18298  grpsubpropd2  19107  mulgpropd  19177  oppglsm  19707  subglsm  19738  lsmpropd  19742  gsumcom2  20040  gsumdixp  20396  funcrngcsetcALT  20740  psrvscafval  22098  evlslem4  22227  evlslem2  22230  psrplusgpropd  22395  mamures  22554  mpomatmul  22603  mamutpos  22615  dmatmul  22654  dmatcrng  22659  scmatscmiddistr  22665  scmatcrng  22678  1marepvmarrepid  22732  1marepvsma1  22740  mdetrsca2  22761  mdetrlin2  22764  mdetunilem5  22773  mdetunilem6  22774  mdetunilem7  22775  mdetunilem8  22776  mdetunilem9  22777  maduval  22795  maducoeval  22796  maducoeval2  22797  madugsum  22800  madurid  22801  smadiadetglem2  22829  cramerimplem2  22841  mat2pmatghm  22887  mat2pmatmul  22888  m2cpminvid  22910  m2cpminvid2  22912  decpmatid  22927  decpmatmulsumfsupp  22930  monmatcollpw  22936  pmatcollpwscmatlem2  22947  mp2pm2mplem3  22965  mp2pm2mplem4  22966  pm2mpghm  22973  pm2mpmhmlem1  22975  ptval2  23758  cnmpt2t  23830  cnmpt22  23831  cnmptcom  23835  cnmptk2  23843  cnmpt2plusg  24245  istgp2  24248  prdstmdd  24281  cnmpt2vsca  24352  cnmpt2ds  25001  cnmpopc  25087  cnmpt2ip  25407  rrxds  25552  rrxmfval  25565  elntg2  29335  nvmfval  30996  elrgspnlem2  33563  fedgmullem2  34020  mdetpmtr12  34215  madjusmdetlem1  34217  pstmval  34285  sseqval  34778  cvmlift2lem6  35800  cvmlift2lem7  35801  cvmlift2lem12  35806  matunitlindflem1  38267  dvhfvadd  41865  fmpocos  43004  2arymaptfo  49434  rrxlinesc  49515  isofval2  49810  oppc1stf  50066  oppc2ndf  50067  tposcurf1  50077  diag1  50082  precofvalALT  50146