Theorem elecALTV

Description: Elementhood in the R -coset of A . Theorem 72 of Suppes p. 82. (I think we should replace elecg with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	elecALTV	|- ( ( A e. V /\ B e. W ) -> ( B e. [ A ] R <-> A R B ) )

Proof

Step	Hyp	Ref	Expression
1		elimasng	|- ( ( A e. V /\ B e. W ) -> ( B e. ( R " { A } ) <-> <. A , B >. e. R ) )
2		df-ec	|- [ A ] R = ( R " { A } )
3	2	eleq2i	|- ( B e. [ A ] R <-> B e. ( R " { A } ) )
4		df-br	|- ( A R B <-> <. A , B >. e. R )
5	1 3 4	3bitr4g	|- ( ( A e. V /\ B e. W ) -> ( B e. [ A ] R <-> A R B ) )