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  9075  iseqovex  9219  iseqid  9247  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrex  9624  climcl  9803  clim2  9804  climuni  9814  climeq  9820  2clim  9822  climshftlemg  9823  climabs0  9828  climcn1  9829  climcn2  9830  climge0  9845  climsqz  9855  climsqz2  9856  climcau  9866  climrecvg1n  9867  climcaucn  9870  serif0  9871  ialginv  9886  ialgfx  9891