Theorem eliniseg

Description: Membership in an initial segment. The idiom (`' A " { B } ) , meaning { x | x A B } ` , is used to specify an initial segment in (for example) Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypothesis	eliniseg.1	|- C e. _V
Assertion	eliniseg	|- ( B e. V -> ( C e. ( `' A " { B } ) <-> C A B ) )

Proof

Step	Hyp	Ref	Expression
1		eliniseg.1	|- C e. _V
2		elimasng	|- ( ( B e. V /\ C e. _V ) -> ( C e. ( `' A " { B } ) <-> <. B , C >. e. `' A ) )
3		df-br	|- ( B `' A C <-> <. B , C >. e. `' A )
4	2 3	bitr4di	|- ( ( B e. V /\ C e. _V ) -> ( C e. ( `' A " { B } ) <-> B `' A C ) )
5		brcnvg	|- ( ( B e. V /\ C e. _V ) -> ( B `' A C <-> C A B ) )
6	4 5	bitrd	|- ( ( B e. V /\ C e. _V ) -> ( C e. ( `' A " { B } ) <-> C A B ) )
7	1 6	mpan2	|- ( B e. V -> ( C e. ( `' A " { B } ) <-> C A B ) )