Theorem mpoeq3ia 7447

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ∈ 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-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  mpodifsnif  7484  mposnif  7485  oprab2co  8053  cnfcomlem  9628  cnfcom2  9631  dfioo2  13387  elovmpowrd  14499  sadcom  16409  comfffval2  17642  oppchomf  17661  symgga  19321  oppglsm  19556  dfrhm2  20394  cnfldsub  21339  cnflddiv  21342  cnflddivOLD  21343  mat0op  22339  mattpos1  22376  mdetunilem7  22538  madufval  22557  maducoeval2  22560  madugsum  22563  mp2pm2mplem5  22730  mp2pm2mp  22731  leordtval  23133  xpstopnlem1  23729  divcnOLD  24790  divcn  24792  oprpiece1res1  24882  oprpiece1res2  24883  ehl1eudis  25353  ehl2eudis  25355  cxpcn  26687  cxpcnOLD  26688  cnnvm  30661  mdetpmtr2  33807  madjusmdetlem1  33810  cnre2csqima  33894  mndpluscn  33909  raddcn  33912  icorempo  37332  matunitlindflem1  37603  mendplusgfval  43163  hoidmv1le  46585  hspdifhsp  46607  vonn0ioo  46678  vonn0icc  46679  dflinc2  48392  cofuoppf  49132  dfswapf2  49243  diag1a  49287  funcsetc1o  49479