Theorem elinisegg

Description: Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Put in closed form and shorten. (Revised by BJ, 16-Oct-2024)

	Ref	Expression
Assertion	elinisegg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elimasng1	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐵 ◡ 𝐴 𝐶 ) )
2		brcnvg	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ◡ 𝐴 𝐶 ↔ 𝐶 𝐴 𝐵 ) )
3	1 2	bitrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )