# Metamath Proof Explorer

## Theorem redundss3

Description: Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Hypothesis redundss3.1 ${⊢}{D}\subseteq {C}$
Assertion redundss3 ${⊢}{A}Redund⟨{B},{C}⟩\to {A}Redund⟨{B},{D}⟩$

### Proof

Step Hyp Ref Expression
1 redundss3.1 ${⊢}{D}\subseteq {C}$
2 ineq1 ${⊢}{A}\cap {C}={B}\cap {C}\to \left({A}\cap {C}\right)\cap {D}=\left({B}\cap {C}\right)\cap {D}$
3 dfss ${⊢}{D}\subseteq {C}↔{D}={D}\cap {C}$
4 1 3 mpbi ${⊢}{D}={D}\cap {C}$
5 incom ${⊢}{D}\cap {C}={C}\cap {D}$
6 4 5 eqtri ${⊢}{D}={C}\cap {D}$
7 6 ineq2i ${⊢}{A}\cap {D}={A}\cap \left({C}\cap {D}\right)$
8 inass ${⊢}\left({A}\cap {C}\right)\cap {D}={A}\cap \left({C}\cap {D}\right)$
9 7 8 eqtr4i ${⊢}{A}\cap {D}=\left({A}\cap {C}\right)\cap {D}$
10 6 ineq2i ${⊢}{B}\cap {D}={B}\cap \left({C}\cap {D}\right)$
11 inass ${⊢}\left({B}\cap {C}\right)\cap {D}={B}\cap \left({C}\cap {D}\right)$
12 10 11 eqtr4i ${⊢}{B}\cap {D}=\left({B}\cap {C}\right)\cap {D}$
13 2 9 12 3eqtr4g ${⊢}{A}\cap {C}={B}\cap {C}\to {A}\cap {D}={B}\cap {D}$
14 13 anim2i ${⊢}\left({A}\subseteq {B}\wedge {A}\cap {C}={B}\cap {C}\right)\to \left({A}\subseteq {B}\wedge {A}\cap {D}={B}\cap {D}\right)$
15 df-redund ${⊢}{A}Redund⟨{B},{C}⟩↔\left({A}\subseteq {B}\wedge {A}\cap {C}={B}\cap {C}\right)$
16 df-redund ${⊢}{A}Redund⟨{B},{D}⟩↔\left({A}\subseteq {B}\wedge {A}\cap {D}={B}\cap {D}\right)$
17 14 15 16 3imtr4i ${⊢}{A}Redund⟨{B},{C}⟩\to {A}Redund⟨{B},{D}⟩$