Metamath Proof Explorer

Theorem bj-opelid

Description: Characterization of the ordered pair elements of the identity relation when the intersection of their components are sets. Note that the antecedent is more general than either component being a set. (Contributed by BJ, 29-Mar-2020)

		Ref	Expression
	Assertion	bj-opelid	$⊢ A \cap B \in V \to (⟨A, B⟩ \in I \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		bj-inexeqex	$⊢ (A \cap B \in V \land A = B) \to (A \in V \land B \in V)$
2	1	ex	$⊢ A \cap B \in V \to (A = B \to (A \in V \land B \in V))$
3		bj-opelidb	$⊢ ⟨A, B⟩ \in I \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		ancr	$⊢ (A = B \to (A \in V \land B \in V)) \to (A = B \to ((A \in V \land B \in V) \land A = B))$
6	4 5	impbid2	$⊢ (A = B \to (A \in V \land B \in V)) \to (((A \in V \land B \in V) \land A = B) \leftrightarrow A = B)$
7	3 6	bitrid	$⊢ (A = B \to (A \in V \land B \in V)) \to (⟨A, B⟩ \in I \leftrightarrow A = B)$
8	2 7	syl	$⊢ A \cap B \in V \to (⟨A, B⟩ \in I \leftrightarrow A = B)$