Metamath Proof Explorer

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⟩ \in I \leftrightarrow ((A \in V \land B \in V) \land A = B)$

Proof

Step	Hyp	Ref	Expression
1		df-id	$⊢ I = \{⟨x, y⟩ \| x = y\}$
2	1	a1i	$⊢ ⊤ \to I = \{⟨x, y⟩ \| x = y\}$
3		eqeq12	$⊢ (x = A \land y = B) \to (x = y \leftrightarrow A = B)$
4	3	adantl	$⊢ (⊤ \land (x = A \land y = B)) \to (x = y \leftrightarrow A = B)$
5	2 4	opelopabbv	$⊢ ⊤ \to (⟨A, B⟩ \in I \leftrightarrow ((A \in V \land B \in V) \land A = B))$
6	5	mptru	$⊢ ⟨A, B⟩ \in I \leftrightarrow ((A \in V \land B \in V) \land A = B)$