Theorem mpoeq3dva 7352

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  {coprab 7276   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-oprab 7279  df-mpo 7280

This theorem is referenced by:  mpoeq3ia  7353  mpoeq3dv  7354  fmpoco  7935  mapxpen  8930  cantnffval  9421  cantnfres  9435  sadfval  16159  smufval  16184  vdwapfval  16672  comfeq  17415  monpropd  17449  cofuval2  17602  cofuass  17604  cofulid  17605  cofurid  17606  catcisolem  17825  prfval  17916  prf1st  17921  prf2nd  17922  1st2ndprf  17923  xpcpropd  17926  curf1  17943  curfuncf  17956  curf2ndf  17965  grpsubpropd2  18681  mulgpropd  18745  oppglsm  19247  subglsm  19279  lsmpropd  19283  gsumcom2  19576  gsumdixp  19848  psrvscafval  21159  evlslem4  21284  evlslem2  21289  psrplusgpropd  21407  mamures  21539  mpomatmul  21595  mamutpos  21607  dmatmul  21646  dmatcrng  21651  scmatscmiddistr  21657  scmatcrng  21670  1marepvmarrepid  21724  1marepvsma1  21732  mdetrsca2  21753  mdetrlin2  21756  mdetunilem5  21765  mdetunilem6  21766  mdetunilem7  21767  mdetunilem8  21768  mdetunilem9  21769  maduval  21787  maducoeval  21788  maducoeval2  21789  madugsum  21792  madurid  21793  smadiadetglem2  21821  cramerimplem2  21833  mat2pmatghm  21879  mat2pmatmul  21880  m2cpminvid  21902  m2cpminvid2  21904  decpmatid  21919  decpmatmulsumfsupp  21922  monmatcollpw  21928  pmatcollpwscmatlem2  21939  mp2pm2mplem3  21957  mp2pm2mplem4  21958  pm2mpghm  21965  pm2mpmhmlem1  21967  ptval2  22752  cnmpt2t  22824  cnmpt22  22825  cnmptcom  22829  cnmptk2  22837  cnmpt2plusg  23239  istgp2  23242  prdstmdd  23275  cnmpt2vsca  23346  cnmpt2ds  24006  cnmpopc  24091  cnmpt2ip  24412  rrxds  24557  rrxmfval  24570  elntg2  27353  nvmfval  29006  fedgmullem2  31711  mdetpmtr12  31775  madjusmdetlem1  31777  pstmval  31845  sseqval  32355  cvmlift2lem6  33270  cvmlift2lem7  33271  cvmlift2lem12  33276  matunitlindflem1  35773  dvhfvadd  39105  funcrngcsetcALT  45557  2arymaptfo  46000  rrxlinesc  46081