Theorem ideq 5852

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

Syntax hints:   ↔ wb 205   = wceq 1540   ∈ wcel 2105  Vcvv 3473   class class class wbr 5148   I cid 5573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683

This theorem is referenced by:  dmi  5921  resieq  5992  iss  6035  elidinxp  6043  restidsing  6052  imai  6073  intasym  6116  asymref  6117  intirr  6119  poirr2  6125  cnvi  6141  xpdifid  6167  coi1  6261  dfpo2  6295  dffun2  6553  dffun2OLD  6554  dffv2  6986  isof1oidb  7324  idssen  8999  dflt2  13134  relexpindlem  15017  opsrtoslem2  21927  hausdiag  23468  hauseqlcld  23469  metustid  24382  ltgov  28280  ex-id  30119  dfso2  35194  idsset  35331  dfon3  35333  elfix  35344  dffix2  35346  sscoid  35354  dffun10  35355  elfuns  35356  brsingle  35358  brapply  35379  brsuccf  35382  dfrdg4  35392  bj-imdiridlem  36529  iss2  37676  undmrnresiss  42817  dffrege99  43175  ipo0  43670  ifr0  43671  fourierdlem42  45323