Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
itgeq1
Next ⟩
nfitg1
Metamath Proof Explorer
Ascii
Unicode
Theorem
itgeq1
Description:
Equality theorem for an integral.
(Contributed by
Mario Carneiro
, 28-Jun-2014)
Ref
Expression
Assertion
itgeq1
⊢
A
=
B
→
∫
A
C
d
x
=
∫
B
C
d
x
Proof
Step
Hyp
Ref
Expression
1
eleq2
⊢
A
=
B
→
x
∈
A
↔
x
∈
B
2
1
anbi1d
⊢
A
=
B
→
x
∈
A
∧
0
≤
y
↔
x
∈
B
∧
0
≤
y
3
2
ifbid
⊢
A
=
B
→
if
x
∈
A
∧
0
≤
y
y
0
=
if
x
∈
B
∧
0
≤
y
y
0
4
3
csbeq2dv
⊢
A
=
B
→
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
=
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
5
4
mpteq2dv
⊢
A
=
B
→
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
=
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
6
5
fveq2d
⊢
A
=
B
→
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
=
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
7
6
oveq2d
⊢
A
=
B
→
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
=
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
8
7
sumeq2sdv
⊢
A
=
B
→
∑
k
=
0
3
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
=
∑
k
=
0
3
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
9
df-itg
⊢
∫
A
C
d
x
=
∑
k
=
0
3
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
A
∧
0
≤
y
y
0
10
df-itg
⊢
∫
B
C
d
x
=
∑
k
=
0
3
i
k
⁢
∫
2
⁡
x
∈
ℝ
⟼
⦋
ℜ
⁡
C
i
k
/
y
⦌
if
x
∈
B
∧
0
≤
y
y
0
11
8
9
10
3eqtr4g
⊢
A
=
B
→
∫
A
C
d
x
=
∫
B
C
d
x