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

Metamath Proof Explorer

Theorem elimasn1

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Use df-br and shorten proof. (Revised by BJ, 16-Oct-2024)

	Ref	Expression
Hypotheses	elimasn1.1	⊢ 𝐵 ∈ V
	elimasn1.2	⊢ 𝐶 ∈ V
Assertion	elimasn1	⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elimasn1.1	⊢ 𝐵 ∈ V
2		elimasn1.2	⊢ 𝐶 ∈ V
3		elimasng1	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )
4	1 2 3	mp2an	⊢ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 )