Theorem ideq 5837

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106   I cid 5550

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663

This theorem is used by:  cnvi  5871  dmi  5911  resieq  5993  iss  6040  elidinxp  6049  restidsing  6058  imai  6085  intasym  6122  asymref  6123  intirr  6125  poirr2  6131  xpdifid  6172  idresdmsscocnv1  6276  coi1  6280  dfpo2  6320  dffun2  6571  dffv2  7006  isof1oidb  7358  idssen  9055  dflt2  13307  relexpindlem  15248  ex-chn1  18843  opsrtoslem2  22398  hausdiag  23997  hauseqlcld  23998  metustid  24906  ltgov  29093  ex-id  31068  dfso2  36711  idsset  36843  dfon3  36845  elfix  36856  dffix2  36858  sscoid  36866  dffun10  36867  elfuns  36868  brsingle  36870  brapply  36891  lemsuccf  36894  dfrdg4  36906  coi1res  38164  bj-imdiridlem  38311  iss2  39479  undmrnresiss  44807  dffrege99  45165  ipo0  45634  ifr0  45635  fourierdlem42  47374