Theorem ideq 5758

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

Hypothesis

Ref	Expression
ideq.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ideq	⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Proof of Theorem ideq

Step	Hyp	Ref	Expression
1		ideq.1	. 2 ⊢ 𝐵 ∈ V
2		ideqg 5757	. 2 ⊢ (𝐵 ∈ V → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2109  Vcvv 3430   class class class wbr 5078   I cid 5487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-id 5488  df-xp 5594  df-rel 5595

This theorem is referenced by:  dmi  5827  resieq  5899  iss  5940  elidinxp  5948  restidsing  5959  imai  5979  intasym  6017  asymref  6018  intirr  6020  poirr2  6026  cnvi  6042  xpdifid  6068  coi1  6163  dfpo2  6196  dffv2  6857  isof1oidb  7188  idssen  8756  dflt2  12864  relexpindlem  14755  opsrtoslem2  21244  hausdiag  22777  hauseqlcld  22778  metustid  23691  ltgov  26939  ex-id  28777  dfso2  33701  idsset  34171  dfon3  34173  elfix  34184  dffix2  34186  sscoid  34194  dffun10  34195  elfuns  34196  brsingle  34198  brapply  34219  brsuccf  34222  dfrdg4  34232  bj-imdiridlem  35335  iss2  36458  undmrnresiss  41165  dffrege99  41523  ipo0  42020  ifr0  42021  fourierdlem42  43644