Theorem bj-opelidb1

Description: Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Assertion	bj-opelidb1	|- ( <. A , B >. e. _I <-> ( A e. _V /\ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		an32	|- ( ( ( A e. _V /\ B e. _V ) /\ A = B ) <-> ( ( A e. _V /\ A = B ) /\ B e. _V ) )
2		bj-opelidb	|- ( <. A , B >. e. _I <-> ( ( A e. _V /\ B e. _V ) /\ A = B ) )
3		eleq1	|- ( A = B -> ( A e. _V <-> B e. _V ) )
4	3	biimpac	|- ( ( A e. _V /\ A = B ) -> B e. _V )
5	4	pm4.71i	|- ( ( A e. _V /\ A = B ) <-> ( ( A e. _V /\ A = B ) /\ B e. _V ) )
6	1 2 5	3bitr4i	|- ( <. A , B >. e. _I <-> ( A e. _V /\ A = B ) )