Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Redundancy
redundss3
Next ⟩
redundeq1
Metamath Proof Explorer
Ascii
Unicode
Theorem
redundss3
Description:
Implication of redundancy predicate.
(Contributed by
Peter Mazsa
, 26-Oct-2022)
Ref
Expression
Hypothesis
redundss3.1
⊢
D
⊆
C
Assertion
redundss3
⊢
A
Redund
B
C
→
A
Redund
B
D
Proof
Step
Hyp
Ref
Expression
1
redundss3.1
⊢
D
⊆
C
2
ineq1
⊢
A
∩
C
=
B
∩
C
→
A
∩
C
∩
D
=
B
∩
C
∩
D
3
dfss
⊢
D
⊆
C
↔
D
=
D
∩
C
4
1
3
mpbi
⊢
D
=
D
∩
C
5
incom
⊢
D
∩
C
=
C
∩
D
6
4
5
eqtri
⊢
D
=
C
∩
D
7
6
ineq2i
⊢
A
∩
D
=
A
∩
C
∩
D
8
inass
⊢
A
∩
C
∩
D
=
A
∩
C
∩
D
9
7
8
eqtr4i
⊢
A
∩
D
=
A
∩
C
∩
D
10
6
ineq2i
⊢
B
∩
D
=
B
∩
C
∩
D
11
inass
⊢
B
∩
C
∩
D
=
B
∩
C
∩
D
12
10
11
eqtr4i
⊢
B
∩
D
=
B
∩
C
∩
D
13
2
9
12
3eqtr4g
⊢
A
∩
C
=
B
∩
C
→
A
∩
D
=
B
∩
D
14
13
anim2i
⊢
A
⊆
B
∧
A
∩
C
=
B
∩
C
→
A
⊆
B
∧
A
∩
D
=
B
∩
D
15
df-redund
⊢
A
Redund
B
C
↔
A
⊆
B
∧
A
∩
C
=
B
∩
C
16
df-redund
⊢
A
Redund
B
D
↔
A
⊆
B
∧
A
∩
D
=
B
∩
D
17
14
15
16
3imtr4i
⊢
A
Redund
B
C
→
A
Redund
B
D