Metamath Proof Explorer

Theorem elimasn

Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by BJ, 16-Oct-2024) TODO: replace existing usages by usages of elimasn1 , remove, and relabel elimasn1 to "elimasn".

Ref Expression
Hypotheses elimasn.1 ⊢ B ∈ V
elimasn.2 ⊢ C ∈ V
Assertion elimasn ⊢ C ∈ A B ↔ B C ∈ A

Proof

Step Hyp Ref Expression
1 elimasn.1 ⊢ B ∈ V
2 elimasn.2 ⊢ C ∈ V
3 elimasng ⊢ B ∈ V ∧ C ∈ V → C ∈ A B ↔ B C ∈ A
4 1 2 3 mp2an ⊢ C ∈ A B ↔ B C ∈ A