Theorem redundeq1

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

	Ref	Expression
Hypothesis	redundeq1.1	|- A = D
Assertion	redundeq1	|- ( A Redund <. B , C >. <-> D Redund <. B , C >. )

Proof

Step	Hyp	Ref	Expression
1		redundeq1.1	|- A = D
2	1	sseq1i	|- ( A C_ B <-> D C_ B )
3	1	ineq1i	|- ( A i^i C ) = ( D i^i C )
4	3	eqeq1i	|- ( ( A i^i C ) = ( B i^i C ) <-> ( D i^i C ) = ( B i^i C ) )
5	2 4	anbi12i	|- ( ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) <-> ( D C_ B /\ ( D i^i C ) = ( B i^i C ) ) )
6		df-redund	|- ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) )
7		df-redund	|- ( D Redund <. B , C >. <-> ( D C_ B /\ ( D i^i C ) = ( B i^i C ) ) )
8	5 6 7	3bitr4i	|- ( A Redund <. B , C >. <-> D Redund <. B , C >. )