Theorem elinlem

Description: Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020)

	Ref	Expression
Assertion	elinlem	|- ( A e. ( B i^i C ) <-> ( A e. B /\ ( _I ` A ) e. C ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
2		fvi	|- ( A e. B -> ( _I ` A ) = A )
3	2	eqcomd	|- ( A e. B -> A = ( _I ` A ) )
4	3	eleq1d	|- ( A e. B -> ( A e. C <-> ( _I ` A ) e. C ) )
5	4	pm5.32i	|- ( ( A e. B /\ A e. C ) <-> ( A e. B /\ ( _I ` A ) e. C ) )
6	1 5	bitri	|- ( A e. ( B i^i C ) <-> ( A e. B /\ ( _I ` A ) e. C ) )