Theorem mpoeq3dva 7446

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 7435	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7374	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7374	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2789	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

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

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 7373  df-mpo 7374

This theorem is referenced by:  mpoeq3ia  7447  mpoeq3dv  7448  fmpoco  8051  mapxpen  9084  cantnffval  9592  cantnfres  9606  sadfval  16398  smufval  16423  vdwapfval  16918  comfeq  17647  monpropd  17679  cofuval2  17829  cofuass  17831  cofulid  17832  cofurid  17833  catcisolem  18052  prfval  18140  prf1st  18145  prf2nd  18146  1st2ndprf  18147  xpcpropd  18149  curf1  18166  curfuncf  18179  curf2ndf  18188  grpsubpropd2  18960  mulgpropd  19030  oppglsm  19556  subglsm  19587  lsmpropd  19591  gsumcom2  19889  gsumdixp  20239  funcrngcsetcALT  20561  psrvscafval  21890  evlslem4  22016  evlslem2  22019  psrplusgpropd  22153  mamures  22317  mpomatmul  22366  mamutpos  22378  dmatmul  22417  dmatcrng  22422  scmatscmiddistr  22428  scmatcrng  22441  1marepvmarrepid  22495  1marepvsma1  22503  mdetrsca2  22524  mdetrlin2  22527  mdetunilem5  22536  mdetunilem6  22537  mdetunilem7  22538  mdetunilem8  22539  mdetunilem9  22540  maduval  22558  maducoeval  22559  maducoeval2  22560  madugsum  22563  madurid  22564  smadiadetglem2  22592  cramerimplem2  22604  mat2pmatghm  22650  mat2pmatmul  22651  m2cpminvid  22673  m2cpminvid2  22675  decpmatid  22690  decpmatmulsumfsupp  22693  monmatcollpw  22699  pmatcollpwscmatlem2  22710  mp2pm2mplem3  22728  mp2pm2mplem4  22729  pm2mpghm  22736  pm2mpmhmlem1  22738  ptval2  23521  cnmpt2t  23593  cnmpt22  23594  cnmptcom  23598  cnmptk2  23606  cnmpt2plusg  24008  istgp2  24011  prdstmdd  24044  cnmpt2vsca  24115  cnmpt2ds  24765  cnmpopc  24855  cnmpt2ip  25181  rrxds  25326  rrxmfval  25339  elntg2  28965  nvmfval  30623  elrgspnlem2  33210  fedgmullem2  33619  mdetpmtr12  33808  madjusmdetlem1  33810  pstmval  33878  sseqval  34372  cvmlift2lem6  35288  cvmlift2lem7  35289  cvmlift2lem12  35294  matunitlindflem1  37603  dvhfvadd  41078  fmpocos  42215  2arymaptfo  48636  rrxlinesc  48717  isofval2  49014  oppc1stf  49270  oppc2ndf  49271  tposcurf1  49281  diag1  49286  precofvalALT  49350