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 \in V \lor B \in W) \to (A I B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		eqeq12	$⊢ (x = A \land y = B) \to (x = y \leftrightarrow A = B)$
2		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
3	1 2	bj-brab2a1	$⊢ A I B \leftrightarrow ((A \in V \land B \in V) \land A = B)$
4		simpr	$⊢ ((A \in V \land B \in V) \land A = B) \to A = B$
5		elex	$⊢ A \in V \to A \in V$
6	5	a1d	$⊢ A \in V \to (A = B \to A \in V)$
7		elex	$⊢ B \in W \to B \in V$
8		eleq1a	$⊢ B \in V \to (A = B \to A \in V)$
9	7 8	syl	$⊢ B \in W \to (A = B \to A \in V)$
10	6 9	jaoi	$⊢ (A \in V \lor B \in W) \to (A = B \to A \in V)$
11		eleq1	$⊢ A = B \to (A \in V \leftrightarrow B \in V)$
12	5 11	syl5ibcom	$⊢ A \in V \to (A = B \to B \in V)$
13	7	a1d	$⊢ B \in W \to (A = B \to B \in V)$
14	12 13	jaoi	$⊢ (A \in V \lor B \in W) \to (A = B \to B \in V)$
15	10 14	jcad	$⊢ (A \in V \lor B \in W) \to (A = B \to (A \in V \land B \in V))$
16	15	ancrd	$⊢ (A \in V \lor B \in W) \to (A = B \to ((A \in V \land B \in V) \land A = B))$
17	4 16	impbid2	$⊢ (A \in V \lor B \in W) \to (((A \in V \land B \in V) \land A = B) \leftrightarrow A = B)$
18	3 17	syl5bb	$⊢ (A \in V \lor B \in W) \to (A I B \leftrightarrow A = B)$