Theorem eltail

Description: An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Hypothesis	tailfval.1	|- X = dom D
Assertion	eltail	|- ( ( D e. DirRel /\ A e. X /\ B e. C ) -> ( B e. ( ( tail ` D ) ` A ) <-> A D B ) )

Proof

Step	Hyp	Ref	Expression
1		tailfval.1	|- X = dom D
2	1	tailval	|- ( ( D e. DirRel /\ A e. X ) -> ( ( tail ` D ) ` A ) = ( D " { A } ) )
3	2	eleq2d	|- ( ( D e. DirRel /\ A e. X ) -> ( B e. ( ( tail ` D ) ` A ) <-> B e. ( D " { A } ) ) )
4	3	3adant3	|- ( ( D e. DirRel /\ A e. X /\ B e. C ) -> ( B e. ( ( tail ` D ) ` A ) <-> B e. ( D " { A } ) ) )
5		elimasng	|- ( ( A e. X /\ B e. C ) -> ( B e. ( D " { A } ) <-> <. A , B >. e. D ) )
6		df-br	|- ( A D B <-> <. A , B >. e. D )
7	5 6	bitr4di	|- ( ( A e. X /\ B e. C ) -> ( B e. ( D " { A } ) <-> A D B ) )
8	7	3adant1	|- ( ( D e. DirRel /\ A e. X /\ B e. C ) -> ( B e. ( D " { A } ) <-> A D B ) )
9	4 8	bitrd	|- ( ( D e. DirRel /\ A e. X /\ B e. C ) -> ( B e. ( ( tail ` D ) ` A ) <-> A D B ) )