Theorem elunii

Description: Membership in class union. (Contributed by NM, 24-Mar-1995)

	Ref	Expression
Assertion	elunii	|- ( ( A e. B /\ B e. C ) -> A e. U. C )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( x = B -> ( A e. x <-> A e. B ) )
2		eleq1	|- ( x = B -> ( x e. C <-> B e. C ) )
3	1 2	anbi12d	|- ( x = B -> ( ( A e. x /\ x e. C ) <-> ( A e. B /\ B e. C ) ) )
4	3	spcegv	|- ( B e. C -> ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) ) )
5	4	anabsi7	|- ( ( A e. B /\ B e. C ) -> E. x ( A e. x /\ x e. C ) )
6		eluni	|- ( A e. U. C <-> E. x ( A e. x /\ x e. C ) )
7	5 6	sylibr	|- ( ( A e. B /\ B e. C ) -> A e. U. C )