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	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
2		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
3	1 2	bj-brab2a1	⊢ ( 𝐴 I 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) )
4		simpr	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
5		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
6	5	a1d	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
7		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
8		eleq1a	⊢ ( 𝐵 ∈ V → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
9	7 8	syl	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
10	6 9	jaoi	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → 𝐴 ∈ V ) )
11		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
12	5 11	syl5ibcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐵 ∈ V ) )
13	7	a1d	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 = 𝐵 → 𝐵 ∈ V ) )
14	12 13	jaoi	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → 𝐵 ∈ V ) )
15	10 14	jcad	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
16	15	ancrd	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ) )
17	4 16	impbid2	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ↔ 𝐴 = 𝐵 ) )
18	3 17	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊 ) → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )