Theorem redundeq1

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

	Ref	Expression
Hypothesis	redundeq1.1	⊢ 𝐴 = 𝐷
Assertion	redundeq1	⊢ ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐷 Redund ⟨ 𝐵 , 𝐶 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		redundeq1.1	⊢ 𝐴 = 𝐷
2	1	sseq1i	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐷 ⊆ 𝐵 )
3	1	ineq1i	⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐷 ∩ 𝐶 )
4	3	eqeq1i	⊢ ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐷 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) )
5	2 4	anbi12i	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝐷 ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )
6		df-redund	⊢ ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )
7		df-redund	⊢ ( 𝐷 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐷 ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )
8	5 6 7	3bitr4i	⊢ ( 𝐴 Redund ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐷 Redund ⟨ 𝐵 , 𝐶 ⟩ )