Theorem mpoeq3dva 7466

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {coprab 7388   ∈ cmpo 7389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  mpoeq3ia  7467  mpoeq3dv  7468  fmpoco  8074  mapxpen  9107  cantnffval  9616  cantnfres  9630  sadfval  16422  smufval  16447  vdwapfval  16942  comfeq  17667  monpropd  17699  cofuval2  17849  cofuass  17851  cofulid  17852  cofurid  17853  catcisolem  18072  prfval  18160  prf1st  18165  prf2nd  18166  1st2ndprf  18167  xpcpropd  18169  curf1  18186  curfuncf  18199  curf2ndf  18208  grpsubpropd2  18978  mulgpropd  19048  oppglsm  19572  subglsm  19603  lsmpropd  19607  gsumcom2  19905  gsumdixp  20228  funcrngcsetcALT  20550  psrvscafval  21857  evlslem4  21983  evlslem2  21986  psrplusgpropd  22120  mamures  22284  mpomatmul  22333  mamutpos  22345  dmatmul  22384  dmatcrng  22389  scmatscmiddistr  22395  scmatcrng  22408  1marepvmarrepid  22462  1marepvsma1  22470  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  mdetunilem6  22504  mdetunilem7  22505  mdetunilem8  22506  mdetunilem9  22507  maduval  22525  maducoeval  22526  maducoeval2  22527  madugsum  22530  madurid  22531  smadiadetglem2  22559  cramerimplem2  22571  mat2pmatghm  22617  mat2pmatmul  22618  m2cpminvid  22640  m2cpminvid2  22642  decpmatid  22657  decpmatmulsumfsupp  22660  monmatcollpw  22666  pmatcollpwscmatlem2  22677  mp2pm2mplem3  22695  mp2pm2mplem4  22696  pm2mpghm  22703  pm2mpmhmlem1  22705  ptval2  23488  cnmpt2t  23560  cnmpt22  23561  cnmptcom  23565  cnmptk2  23573  cnmpt2plusg  23975  istgp2  23978  prdstmdd  24011  cnmpt2vsca  24082  cnmpt2ds  24732  cnmpopc  24822  cnmpt2ip  25148  rrxds  25293  rrxmfval  25306  elntg2  28912  nvmfval  30573  elrgspnlem2  33194  fedgmullem2  33626  mdetpmtr12  33815  madjusmdetlem1  33817  pstmval  33885  sseqval  34379  cvmlift2lem6  35295  cvmlift2lem7  35296  cvmlift2lem12  35301  matunitlindflem1  37610  dvhfvadd  41085  fmpocos  42222  2arymaptfo  48643  rrxlinesc  48724  isofval2  49021  oppc1stf  49277  oppc2ndf  49278  tposcurf1  49288  diag1  49293  precofvalALT  49357