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 ( 𝐵𝑉 → ( 𝐴 I 𝐵𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 id ( 𝐵𝑉𝐵𝑉 )
2 reli Rel I
3 2 brrelex1i ( 𝐴 I 𝐵𝐴 ∈ V )
4 1 3 anim12ci ( ( 𝐵𝑉𝐴 I 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵𝑉 ) )
5 eleq1 ( 𝐴 = 𝐵 → ( 𝐴𝑉𝐵𝑉 ) )
6 5 biimparc ( ( 𝐵𝑉𝐴 = 𝐵 ) → 𝐴𝑉 )
7 6 elexd ( ( 𝐵𝑉𝐴 = 𝐵 ) → 𝐴 ∈ V )
8 simpl ( ( 𝐵𝑉𝐴 = 𝐵 ) → 𝐵𝑉 )
9 7 8 jca ( ( 𝐵𝑉𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵𝑉 ) )
10 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦𝐴 = 𝑦 ) )
11 eqeq2 ( 𝑦 = 𝐵 → ( 𝐴 = 𝑦𝐴 = 𝐵 ) )
12 df-id I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
13 10 11 12 brabg ( ( 𝐴 ∈ V ∧ 𝐵𝑉 ) → ( 𝐴 I 𝐵𝐴 = 𝐵 ) )
14 4 9 13 pm5.21nd ( 𝐵𝑉 → ( 𝐴 I 𝐵𝐴 = 𝐵 ) )