Theorem chnrin2

Description: Distribution of chain class constructor over relation intersection. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chnrin2	|- ( ( R i^i .< ) Chain B ) = ( ( R Chain B ) i^i ( .< Chain B ) )

Proof

Step	Hyp	Ref	Expression
1		chnrrin	|- ( n e. ( ( R i^i .< ) Chain B ) -> ( n e. ( R Chain B ) /\ n e. ( .< Chain B ) ) )
2		chnrin	|- ( ( n e. ( R Chain B ) /\ n e. ( .< Chain B ) ) -> n e. ( ( R i^i .< ) Chain B ) )
3	1 2	impbii	|- ( n e. ( ( R i^i .< ) Chain B ) <-> ( n e. ( R Chain B ) /\ n e. ( .< Chain B ) ) )
4		elin	|- ( n e. ( ( R Chain B ) i^i ( .< Chain B ) ) <-> ( n e. ( R Chain B ) /\ n e. ( .< Chain B ) ) )
5	3 4	bitr4i	|- ( n e. ( ( R i^i .< ) Chain B ) <-> n e. ( ( R Chain B ) i^i ( .< Chain B ) ) )
6	5	eqriv	|- ( ( R i^i .< ) Chain B ) = ( ( R Chain B ) i^i ( .< Chain B ) )