Theorem mpoeq3ia 7488

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpoeq3ia.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpoeq3ia	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Proof of Theorem mpoeq3ia

Step	Hyp	Ref	Expression
1		mpoeq3ia.1	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
2	1	3adant1 1148	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7487	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
4	3	mptru 1577	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ⊤wtru 1571   ∈ wcel 2143   ∈ 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-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-oprab 7414  df-mpo 7415

This theorem is referenced by:  mpodifsnif  7525  mposnif  7526  oprab2co  8088  cnfcomlem  9664  cnfcom2  9667  dfioo2  13472  elovmpowrd  14591  sadcom  16516  comfffval2  17752  oppchomf  17771  symgga  19472  oppglsm  19707  dfrhm2  20552  cnfldsub  21550  cnflddiv  21552  mat0op  22576  mattpos1  22613  mdetunilem7  22775  madufval  22794  maducoeval2  22797  madugsum  22800  mp2pm2mplem5  22967  mp2pm2mp  22968  leordtval  23370  xpstopnlem1  23966  divcn  25027  oprpiece1res1  25110  oprpiece1res2  25111  ehl1eudis  25579  ehl2eudis  25581  cxpcn  26910  cnnvm  31034  issply  33951  mdetpmtr2  34214  madjusmdetlem1  34217  cnre2csqima  34301  mndpluscn  34316  raddcn  34319  icorempo  38017  matunitlindflem1  38287  mendplusgfval  43928  hoidmv1le  47328  hspdifhsp  47350  vonn0ioo  47421  vonn0icc  47422  dflinc2  49210  cofuoppf  49948  dfswapf2  50059  diag1a  50103  funcsetc1o  50295