Theorem redundeq1

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

	Ref	Expression
Hypothesis	redundeq1.1	$$⊢A=D$$
Assertion	redundeq1	$$⊢ARedund⟨B,C⟩\leftrightarrow DRedund⟨B,C⟩$$

Proof

Step	Hyp	Ref	Expression
1		redundeq1.1	$$⊢A=D$$
2	1	sseq1i	$$⊢A\subseteq B\leftrightarrow D\subseteq B$$
3	1	ineq1i	$$⊢A\cap C=D\cap C$$
4	3	eqeq1i	$$⊢A\cap C=B\cap C\leftrightarrow D\cap C=B\cap C$$
5	2 4	anbi12i	$$⊢\left(A\subseteq B\wedge A\cap C=B\cap C\right)\leftrightarrow \left(D\subseteq B\wedge D\cap C=B\cap C\right)$$
6		df-redund	$$⊢ARedund⟨B,C⟩\leftrightarrow \left(A\subseteq B\wedge A\cap C=B\cap C\right)$$
7		df-redund	$$⊢DRedund⟨B,C⟩\leftrightarrow \left(D\subseteq B\wedge D\cap C=B\cap C\right)$$
8	5 6 7	3bitr4i	$$⊢ARedund⟨B,C⟩\leftrightarrow DRedund⟨B,C⟩$$