Theorem ideq 5809

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 5808	. 2 ⊢ (𝐵 ∈ V → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100   I cid 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639

This theorem is referenced by:  dmi  5878  resieq  5957  iss  6002  elidinxp  6011  restidsing  6020  imai  6041  intasym  6080  asymref  6081  intirr  6083  poirr2  6089  cnvi  6107  xpdifid  6134  coi1  6229  dfpo2  6262  dffun2  6510  dffv2  6937  isof1oidb  7280  idssen  8946  dflt2  13074  relexpindlem  14998  ex-chn1  18572  opsrtoslem2  22023  hausdiag  23601  hauseqlcld  23602  metustid  24510  ltgov  28681  ex-id  30521  dfso2  35968  idsset  36101  dfon3  36103  elfix  36114  dffix2  36116  sscoid  36124  dffun10  36125  elfuns  36126  brsingle  36128  brapply  36149  lemsuccf  36152  dfrdg4  36164  bj-imdiridlem  37434  iss2  38589  undmrnresiss  43954  dffrege99  44312  ipo0  44798  ifr0  44799  fourierdlem42  46501