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	⊢ 𝐶 ∈ V
Assertion	eliniseg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eliniseg.1	⊢ 𝐶 ∈ V
2		elinisegg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )
3	1 2	mpan2	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )