Theorem iniseg

Description: An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 28-Apr-2004)

	Ref	Expression
Assertion	iniseg	|- ( B e. V -> ( `' A " { B } ) = { x | x A B } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( B e. V -> B e. _V )
2		vex	|- x e. _V
3	2	eliniseg	|- ( B e. _V -> ( x e. ( `' A " { B } ) <-> x A B ) )
4	3	abbi2dv	|- ( B e. _V -> ( `' A " { B } ) = { x | x A B } )
5	1 4	syl	|- ( B e. V -> ( `' A " { B } ) = { x | x A B } )