Metamath Proof Explorer


Theorem bj-ideqg1

Description: For sets, the identity relation is the same thing as equality. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) Generalize to a disjunctive antecedent. (Revised by BJ, 24-Dec-2023)

TODO: delete once bj-ideqg is in the main section.

Ref Expression
Assertion bj-ideqg1 AVBWAIBA=B

Proof

Step Hyp Ref Expression
1 eqeq12 x=Ay=Bx=yA=B
2 df-id I=xy|x=y
3 1 2 bj-brab2a1 AIBAVBVA=B
4 simpr AVBVA=BA=B
5 elex AVAV
6 5 a1d AVA=BAV
7 elex BWBV
8 eleq1a BVA=BAV
9 7 8 syl BWA=BAV
10 6 9 jaoi AVBWA=BAV
11 eleq1 A=BAVBV
12 5 11 syl5ibcom AVA=BBV
13 7 a1d BWA=BBV
14 12 13 jaoi AVBWA=BBV
15 10 14 jcad AVBWA=BAVBV
16 15 ancrd AVBWA=BAVBVA=B
17 4 16 impbid2 AVBWAVBVA=BA=B
18 3 17 syl5bb AVBWAIBA=B