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 >. e. _I <-> ( A e. _V /\ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A _I B <-> <. A , B >. e. _I )
2		reli	|- Rel _I
3	2	brrelex1i	|- ( A _I B -> A e. _V )
4	1 3	sylbir	|- ( <. A , B >. e. _I -> A e. _V )
5		inex1g	|- ( A e. _V -> ( A i^i B ) e. _V )
6		bj-opelid	|- ( ( A i^i B ) e. _V -> ( <. A , B >. e. _I <-> A = B ) )
7	5 6	syl	|- ( A e. _V -> ( <. A , B >. e. _I <-> A = B ) )
8	4 7	biadanii	|- ( <. A , B >. e. _I <-> ( A e. _V /\ A = B ) )