Metamath Proof Explorer


Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006)

Ref Expression
Assertion elimasng B V C W C A B B C A

Proof

Step Hyp Ref Expression
1 sneq y = B y = B
2 1 imaeq2d y = B A y = A B
3 2 eleq2d y = B z A y z A B
4 opeq1 y = B y z = B z
5 4 eleq1d y = B y z A B z A
6 3 5 bibi12d y = B z A y y z A z A B B z A
7 eleq1 z = C z A B C A B
8 opeq2 z = C B z = B C
9 8 eleq1d z = C B z A B C A
10 7 9 bibi12d z = C z A B B z A C A B B C A
11 vex y V
12 vex z V
13 11 12 elimasn z A y y z A
14 6 10 13 vtocl2g B V C W C A B B C A