Metamath Proof Explorer

Theorem elimasng1

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) Revise to use df-br and to prove elimasn1 from it. (Revised by BJ, 16-Oct-2024)

Ref Expression
Assertion elimasng1 ⊢ B ∈ V ∧ C ∈ W → C ∈ A B ↔ B A C

Proof

Step Hyp Ref Expression
1 simpr ⊢ B ∈ V ∧ C ∈ W → C ∈ W
2 imasng ⊢ B ∈ V → A B = x | B A x
3 2 adantr ⊢ B ∈ V ∧ C ∈ W → A B = x | B A x
4 simpr ⊢ B ∈ V ∧ C ∈ W ∧ x = C → x = C
5 4 breq2d ⊢ B ∈ V ∧ C ∈ W ∧ x = C → B A x ↔ B A C
6 1 3 5 elabd2 ⊢ B ∈ V ∧ C ∈ W → C ∈ A B ↔ B A C