Metamath Proof Explorer


Theorem eqoreldif

Description: An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Assertion eqoreldif BCACA=BACB

Proof

Step Hyp Ref Expression
1 simpl AC¬A=BAC
2 elsni ABA=B
3 2 con3i ¬A=B¬AB
4 3 adantl AC¬A=B¬AB
5 1 4 eldifd AC¬A=BACB
6 5 ex AC¬A=BACB
7 6 orrd ACA=BACB
8 eleq1a BCA=BAC
9 eldifi ACBAC
10 9 a1i BCACBAC
11 8 10 jaod BCA=BACBAC
12 7 11 impbid2 BCACA=BACB