Metamath Proof Explorer

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 ∈ I ↔ A ∈ V ∧ A = B

Proof

Step Hyp Ref Expression
1 an32 ⊢ A ∈ V ∧ B ∈ V ∧ A = B ↔ A ∈ V ∧ A = B ∧ B ∈ V
2 bj-opelidb ⊢ A B ∈ I ↔ A ∈ V ∧ B ∈ V ∧ A = B
3 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
4 3 biimpac ⊢ A ∈ V ∧ A = B → B ∈ V
5 4 pm4.71i ⊢ A ∈ V ∧ A = B ↔ A ∈ V ∧ A = B ∧ B ∈ V
6 1 2 5 3bitr4i ⊢ A B ∈ I ↔ A ∈ V ∧ A = B