Theorem ideq 5843

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  Vcvv 3458   class class class wbr 5114   I cid 5560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673

This theorem is used by:  cnvi  5876  dmi  5916  resieq  5994  iss  6042  elidinxp  6051  restidsing  6060  imai  6081  intasym  6120  asymref  6121  intirr  6123  poirr2  6129  xpdifid  6170  coi1  6269  dfpo2  6304  dffun2  6553  dffv2  6983  isof1oidb  7333  idssen  9003  dflt2  13191  relexpindlem  15126  ex-chn1  18718  opsrtoslem2  22244  hausdiag  23839  hauseqlcld  23840  metustid  24748  ltgov  28903  ex-id  30822  dfso2  36268  idsset  36401  dfon3  36403  elfix  36414  dffix2  36416  sscoid  36424  dffun10  36425  elfuns  36426  brsingle  36428  brapply  36449  lemsuccf  36452  dfrdg4  36464  bj-imdiridlem  37870  iss2  39034  undmrnresiss  44371  dffrege99  44729  ipo0  45199  ifr0  45200  fourierdlem42  46904