Metamath Proof Explorer

Theorem bj-idreseqb

Description: Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023)

Ref Expression
Assertion bj-idreseqb ⊢ A I ↾ C B ↔ A ∈ C ∧ A = B

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ I ↾ C
2 1 brrelex12i ⊢ A I ↾ C B → A ∈ V ∧ B ∈ V
3 simpl ⊢ A ∈ C ∧ A = B → A ∈ C
4 3 elexd ⊢ A ∈ C ∧ A = B → A ∈ V
5 eleq1 ⊢ A = B → A ∈ C ↔ B ∈ C
6 5 biimpac ⊢ A ∈ C ∧ A = B → B ∈ C
7 6 elexd ⊢ A ∈ C ∧ A = B → B ∈ V
8 4 7 jca ⊢ A ∈ C ∧ A = B → A ∈ V ∧ B ∈ V
9 brres ⊢ B ∈ V → A I ↾ C B ↔ A ∈ C ∧ A I B
10 9 adantl ⊢ A ∈ V ∧ B ∈ V → A I ↾ C B ↔ A ∈ C ∧ A I B
11 eqeq12 ⊢ x = A ∧ y = B → x = y ↔ A = B
12 df-id ⊢ I = x y | x = y
13 11 12 brabga ⊢ A ∈ V ∧ B ∈ V → A I B ↔ A = B
14 13 anbi2d ⊢ A ∈ V ∧ B ∈ V → A ∈ C ∧ A I B ↔ A ∈ C ∧ A = B
15 10 14 bitrd ⊢ A ∈ V ∧ B ∈ V → A I ↾ C B ↔ A ∈ C ∧ A = B
16 2 8 15 pm5.21nii ⊢ A I ↾ C B ↔ A ∈ C ∧ A = B