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

Metamath Proof Explorer

Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) TODO: replace existing usages by usages of elimasng1 , remove, and relabel elimasng1 to "elimasng".

		Ref	Expression
	Assertion	elimasng	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elimasng1	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )
2		df-br	⊢ ( 𝐵 𝐴 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 )
3	1 2	bitrdi	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) )