Theorem eqidd 2041

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2040	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  cbvraldva  2539  cbvrexdva  2540  nelrdva  2746  opeq2  3550  mpteq1  3841  tfisi  4310  feq23d  5042  fvmptdv2  5260  elrnrexdm  5306  fmptco  5330  ftpg  5347  fliftfun  5436  fliftval  5440  cbvmpt2  5583  eqfnov2  5608  ovmpt2d  5628  ovmpt2dv2  5634  fnofval  5721  ofrval  5722  off  5724  ofres  5725  suppssof1  5728  ofco  5729  caofref  5732  caofrss  5735  caoftrn  5736  rdgivallem  5968  iserd  6132  fzo0to3tp  9073  iseqovex  9193  iseqid  9221  resqrexlemp1rp  9578  resqrexlemfp1  9581  resqrex  9598  climcl  9777  clim2  9778  climuni  9788  climeq  9794  2clim  9796  climshftlemg  9797  climabs0  9802  climcn1  9803  climcn2  9804  climge0  9819  climsqz  9829  climsqz2  9830  climcau  9840  climrecvg1n  9841  climcaucn  9844  serif0  9845  ialginv  9860  ialgfx  9865