Theorem bj-opelidb

Description: Characterization of the ordered pair elements of the identity relation.

Remark: in deduction-style proofs, one could save a few syntactic steps by using another antecedent than T. which already appears in the proof. Here for instance this could be the definition _I = { <. x , y >. | x = y } but this would make the proof less easy to read. (Contributed by BJ, 27-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		df-id	|- _I = { <. x , y >. | x = y }
2	1	a1i	|- ( T. -> _I = { <. x , y >. | x = y } )
3		eqeq12	|- ( ( x = A /\ y = B ) -> ( x = y <-> A = B ) )
4	3	adantl	|- ( ( T. /\ ( x = A /\ y = B ) ) -> ( x = y <-> A = B ) )
5	2 4	opelopabbv	|- ( T. -> ( <. A , B >. e. _I <-> ( ( A e. _V /\ B e. _V ) /\ A = B ) ) )
6	5	mptru	|- ( <. A , B >. e. _I <-> ( ( A e. _V /\ B e. _V ) /\ A = B ) )