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

Metamath Proof Explorer

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 proof. (Revised by BJ, 16-Oct-2024)

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

Proof

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