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

Metamath Proof Explorer

Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) TODO: replace existing usages by usages of elimasng1 , remove, and relabel elimasng1 to "elimasng".

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

Proof

Step Hyp Ref Expression
1 elimasng1 ⊢ B ∈ V ∧ C ∈ W → C ∈ A B ↔ B A C
2 df-br ⊢ B A C ↔ B C ∈ A
3 1 2 bitrdi ⊢ B ∈ V ∧ C ∈ W → C ∈ A B ↔ B C ∈ A