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 ⊢ A ∈ V ∨ B ∈ W → A I B ↔ A = B

Proof

Step Hyp Ref Expression
1 eqeq12 ⊢ x = A ∧ y = B → x = y ↔ A = B
2 df-id ⊢ I = x y | x = y
3 1 2 bj-brab2a1 ⊢ A I B ↔ A ∈ V ∧ B ∈ V ∧ A = B
4 simpr ⊢ A ∈ V ∧ B ∈ V ∧ A = B → A = B
5 elex ⊢ A ∈ V → A ∈ V
6 5 a1d ⊢ A ∈ V → A = B → A ∈ V
7 elex ⊢ B ∈ W → B ∈ V
8 eleq1a ⊢ B ∈ V → A = B → A ∈ V
9 7 8 syl ⊢ B ∈ W → A = B → A ∈ V
10 6 9 jaoi ⊢ A ∈ V ∨ B ∈ W → A = B → A ∈ V
11 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
12 5 11 syl5ibcom ⊢ A ∈ V → A = B → B ∈ V
13 7 a1d ⊢ B ∈ W → A = B → B ∈ V
14 12 13 jaoi ⊢ A ∈ V ∨ B ∈ W → A = B → B ∈ V
15 10 14 jcad ⊢ A ∈ V ∨ B ∈ W → A = B → A ∈ V ∧ B ∈ V
16 15 ancrd ⊢ A ∈ V ∨ B ∈ W → A = B → A ∈ V ∧ B ∈ V ∧ A = B
17 4 16 impbid2 ⊢ A ∈ V ∨ B ∈ W → A ∈ V ∧ B ∈ V ∧ A = B ↔ A = B
18 3 17 bitrid ⊢ A ∈ V ∨ B ∈ W → A I B ↔ A = B