Theorem mpoeq3ia 7438

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 1137	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7437	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
4	3	mptru 1555	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548  ⊤wtru 1549   ∈ wcel 2121   ∈ cmpo 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  mpodifsnif  7475  mposnif  7476  oprab2co  8040  cnfcomlem  9615  cnfcom2  9618  dfioo2  13398  elovmpowrd  14515  sadcom  16427  comfffval2  17662  oppchomf  17681  symgga  19377  oppglsm  19612  dfrhm2  20449  cnfldsub  21379  cnflddiv  21381  mat0op  22406  mattpos1  22443  mdetunilem7  22605  madufval  22624  maducoeval2  22627  madugsum  22630  mp2pm2mplem5  22797  mp2pm2mp  22798  leordtval  23200  xpstopnlem1  23796  divcn  24857  oprpiece1res1  24940  oprpiece1res2  24941  ehl1eudis  25409  ehl2eudis  25411  cxpcn  26731  cnnvm  30775  issply  33757  mdetpmtr2  34020  madjusmdetlem1  34023  cnre2csqima  34107  mndpluscn  34122  raddcn  34125  icorempo  37728  matunitlindflem1  37998  mendplusgfval  43641  hoidmv1le  47051  hspdifhsp  47073  vonn0ioo  47144  vonn0icc  47145  dflinc2  48915  cofuoppf  49654  dfswapf2  49765  diag1a  49809  funcsetc1o  50001