This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ideqg

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ideqg ⊢ B ∈ V → A I B ↔ A = B

Proof

Step Hyp Ref Expression
1 id ⊢ B ∈ V → B ∈ V
2 reli ⊢ Rel ⁡ I
3 2 brrelex1i ⊢ A I B → A ∈ V
4 1 3 anim12ci ⊢ B ∈ V ∧ A I B → A ∈ V ∧ B ∈ V
5 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
6 5 biimparc ⊢ B ∈ V ∧ A = B → A ∈ V
7 6 elexd ⊢ B ∈ V ∧ A = B → A ∈ V
8 simpl ⊢ B ∈ V ∧ A = B → B ∈ V
9 7 8 jca ⊢ B ∈ V ∧ A = B → A ∈ V ∧ B ∈ V
10 eqeq1 ⊢ x = A → x = y ↔ A = y
11 eqeq2 ⊢ y = B → A = y ↔ A = B
12 df-id ⊢ I = x y | x = y
13 10 11 12 brabg ⊢ A ∈ V ∧ B ∈ V → A I B ↔ A = B
14 4 9 13 pm5.21nd ⊢ B ∈ V → A I B ↔ A = B