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 ⊢ B ∈ V
elimasn1.2 ⊢ C ∈ V
Assertion elimasn1 ⊢ C ∈ A B ↔ B A C

Proof

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