Theorem eliniseg

Description: Membership in the inverse image of a singleton. An application is to express initial segments for an order relation. See 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		elinisegg	|- ( ( B e. V /\ C e. _V ) -> ( C e. ( `' A " { B } ) <-> C A B ) )
3	1 2	mpan2	|- ( B e. V -> ( C e. ( `' A " { B } ) <-> C A B ) )