Metamath Proof Explorer

Theorem ideq

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995)

Ref Expression
Hypothesis ideq.1 B V
Assertion ideq A I B A = B


Step Hyp Ref Expression
1 ideq.1 B V
2 ideqg B V A I B A = B
3 1 2 ax-mp A I B A = B