Metamath Proof Explorer

Theorem brredundsredund

Description: For sets, binary relation on the class of all redundant sets ( brredunds ) is equivalent to satisfying the redundancy predicate ( df-redund ). (Contributed by Peter Mazsa, 25-Oct-2022)

		Ref	Expression
	Assertion	brredundsredund	\|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> A Redund <. B , C >. ) )

Proof

Step	Hyp	Ref	Expression
1		brredunds	\|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) )
2		df-redund	\|- ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) )
3	1 2	bitr4di	\|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> A Redund <. B , C >. ) )

Step

Hyp

Ref

Expression

brredunds

 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) )

df-redund

 |-  ( A Redund <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) )

1 2

bitr4di

 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> A Redund <. B , C >. ) )