This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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