Theorem mpoeq3ia 7467

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ∈ cmpo 7389

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 7391  df-mpo 7392

This theorem is referenced by:  mpodifsnif  7504  mposnif  7505  oprab2co  8076  cnfcomlem  9652  cnfcom2  9655  dfioo2  13411  elovmpowrd  14523  sadcom  16433  comfffval2  17662  oppchomf  17681  symgga  19337  oppglsm  19572  dfrhm2  20383  cnfldsub  21309  cnflddiv  21312  cnflddivOLD  21313  mat0op  22306  mattpos1  22343  mdetunilem7  22505  madufval  22524  maducoeval2  22527  madugsum  22530  mp2pm2mplem5  22697  mp2pm2mp  22698  leordtval  23100  xpstopnlem1  23696  divcnOLD  24757  divcn  24759  oprpiece1res1  24849  oprpiece1res2  24850  ehl1eudis  25320  ehl2eudis  25322  cxpcn  26654  cxpcnOLD  26655  cnnvm  30611  mdetpmtr2  33814  madjusmdetlem1  33817  cnre2csqima  33901  mndpluscn  33916  raddcn  33919  icorempo  37339  matunitlindflem1  37610  mendplusgfval  43170  hoidmv1le  46592  hspdifhsp  46614  vonn0ioo  46685  vonn0icc  46686  dflinc2  48399  cofuoppf  49139  dfswapf2  49250  diag1a  49294  funcsetc1o  49486