Theorem eqidd 2019

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

Assertion

Ref	Expression
eqidd	⊢ (φ → A = A)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2018	. 2 ⊢ A = A
2	1	a1i 9	1 ⊢ (φ → A = A)

Syntax hints:   → wi 4   = wceq 1226

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 1314  ax-ext 2000

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

This theorem is referenced by:  cbvraldva  2513  cbvrexdva  2514  nelrdva  2719  opeq2  3520  mpteq1  3811  tfisi  4233  feq23d  4964  fvmptdv2  5181  elrnrexdm  5227  fmptco  5251  ftpg  5268  fliftfun  5357  fliftval  5361  cbvmpt2  5502  eqfnov2  5527  ovmpt2d  5547  ovmpt2dv2  5553  fnofval  5640  ofrval  5641  off  5643  ofres  5644  suppssof1  5647  ofco  5648  caofref  5651  caofrss  5654  caoftrn  5655  rdgivallem  5884  iserd  6039