Theorem mpoeq3dva 7501

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {coprab 7425   ∈ cmpo 7426

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-oprab 7428  df-mpo 7429

This theorem is used by:  mpoeq3ia  7502  mpoeq3dv  7503  fmpoco  8112  mapxpen  9170  cantnffval  9671  cantnfres  9685  sadfval  16631  smufval  16656  vdwapfval  17158  comfeq  17889  monpropd  17921  cofuval2  18071  cofuass  18073  cofulid  18074  cofurid  18075  catcisolem  18294  prfval  18382  prf1st  18387  prf2nd  18388  1st2ndprf  18389  xpcpropd  18391  curf1  18408  curfuncf  18421  curf2ndf  18430  grpsubpropd2  19265  mulgpropd  19335  oppglsm  19865  subglsm  19896  lsmpropd  19900  gsumcom2  20198  gsumdixp  20557  funcrngcsetcALT  20902  psrvscafval  22265  evlslem4  22394  evlslem2  22397  psrplusgpropd  22562  mamures  22721  mpomatmul  22770  mamutpos  22782  dmatmul  22821  dmatcrng  22826  scmatscmiddistr  22832  scmatcrng  22845  1marepvmarrepid  22899  1marepvsma1  22907  mdetrsca2  22928  mdetrlin2  22931  mdetunilem5  22940  mdetunilem6  22941  mdetunilem7  22942  mdetunilem8  22943  mdetunilem9  22944  maduval  22962  maducoeval  22963  maducoeval2  22964  madugsum  22967  madurid  22968  smadiadetglem2  22996  matunitlindflem1  23003  cramerimplem2  23011  mat2pmatghm  23057  mat2pmatmul  23058  m2cpminvid  23080  m2cpminvid2  23082  decpmatid  23097  decpmatmulsumfsupp  23100  monmatcollpw  23106  pmatcollpwscmatlem2  23117  mp2pm2mplem3  23135  mp2pm2mplem4  23136  pm2mpghm  23143  pm2mpmhmlem1  23145  ptval2  23929  cnmpt2t  24001  cnmpt22  24002  cnmptcom  24006  cnmptk2  24014  cnmpt2plusg  24416  istgp2  24419  prdstmdd  24452  cnmpt2vsca  24523  cnmpt2ds  25172  cnmpopc  25258  cnmpt2ip  25578  rrxds  25723  rrxmfval  25736  elntg2  29572  nvmfval  31255  elrgspnlem2  33854  fedgmullem2  34312  mdetpmtr12  34507  madjusmdetlem1  34509  pstmval  34577  sseqval  35070  cvmlift2lem6  36191  cvmlift2lem7  36192  cvmlift2lem12  36197  dvhfvadd  42285  fmpocos  43424  2arymaptfo  49902  rrxlinesc  49984  isofval2  50282  oppc1stf  50546  oppc2ndf  50547  tposcurf1  50557  diag1  50562  precofvalALT  50639