Metamath Proof Explorer

Theorem bj-opelidb1ALT

Description: Characterization of the couples in _I . (Contributed by BJ, 29-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ A I B \leftrightarrow ⟨A, B⟩ \in I$
2		reli	$⊢ Rel I$
3	2	brrelex1i	$⊢ A I B \to A \in V$
4	1 3	sylbir	$⊢ ⟨A, B⟩ \in I \to A \in V$
5		inex1g	$⊢ A \in V \to A \cap B \in V$
6		bj-opelid	$⊢ A \cap B \in V \to (⟨A, B⟩ \in I \leftrightarrow A = B)$
7	5 6	syl	$⊢ A \in V \to (⟨A, B⟩ \in I \leftrightarrow A = B)$
8	4 7	biadanii	$⊢ ⟨A, B⟩ \in I \leftrightarrow (A \in V \land A = B)$