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\in \mathrm{V}$$
Assertion	eliniseg	$$⊢B\in V\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$

Proof

Step	Hyp	Ref	Expression
1		eliniseg.1	$$⊢C\in \mathrm{V}$$
2		elinisegg	$$⊢\left(B\in V\wedge C\in \mathrm{V}\right)\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$
3	1 2	mpan2	$$⊢B\in V\to \left(C\in A^{-1}\left[\left\{B\right\}\right]\leftrightarrow CAB\right)$$