Theorem elin3

Description: Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypothesis	elin3.x	|- X = ( ( B i^i C ) i^i D )
Assertion	elin3	|- ( A e. X <-> ( A e. B /\ A e. C /\ A e. D ) )

Proof

Step	Hyp	Ref	Expression
1		elin3.x	|- X = ( ( B i^i C ) i^i D )
2		elin	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
3	2	anbi1i	|- ( ( A e. ( B i^i C ) /\ A e. D ) <-> ( ( A e. B /\ A e. C ) /\ A e. D ) )
4	1	elin2	|- ( A e. X <-> ( A e. ( B i^i C ) /\ A e. D ) )
5		df-3an	|- ( ( A e. B /\ A e. C /\ A e. D ) <-> ( ( A e. B /\ A e. C ) /\ A e. D ) )
6	3 4 5	3bitr4i	|- ( A e. X <-> ( A e. B /\ A e. C /\ A e. D ) )