Theorem chndin2

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

	Ref	Expression
Assertion	chndin2	|- ( R Chain ( B i^i C ) ) = ( ( R Chain B ) i^i ( R Chain C ) )

Proof

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