Theorem eqidd 2190

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 2189	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  cbvraldva  2727  cbvrexdva  2728  rspcedeq1vd  2865  rspcedeq2vd  2866  nelrdva  2959  opeq2  3794  mpteq1  4102  tfisi  4601  feq23d  5376  fvmptdv2  5621  elrnrexdm  5671  fmptco  5698  cofmpt  5701  ftpg  5716  fliftfun  5813  fliftval  5817  cbvmpo  5970  fconstmpo  5986  eqfnov2  5999  ovmpod  6019  ovmpodv2  6025  ofvalg  6110  ofrval  6111  off  6113  ofres  6115  suppssof1  6118  ofco  6119  caofref  6122  caofrss  6125  caoftrn  6126  rdgivallem  6400  iserd  6579  ixpsnf1o  6754  1domsn  6837  mapxpen  6866  infnninf  7140  ctssexmid  7166  nninfdcinf  7187  nninfwlporlemd  7188  nninfwlporlem  7189  nninfwlpoimlemginf  7192  infrenegsupex  9612  fz0to4untppr  10142  fzo0to3tp  10237  modqsubmod  10400  0tonninf  10457  iseqovex  10474  seqvalcd  10477  seq3f1olemqsumkj  10516  seq3id  10526  seq3id2  10527  resqrexlemp1rp  11033  resqrexlemfp1  11036  resqrex  11053  infxrnegsupex  11289  climcl  11308  clim2  11309  climuni  11319  climeq  11325  2clim  11327  climshftlemg  11328  climabs0  11333  climcn1  11334  climcn2  11335  climge0  11351  climsqz  11361  climsqz2  11362  climcau  11373  climrecvg1n  11374  climcaucn  11377  serf0  11378  isumz  11415  fisumss  11418  fsumsplitsn  11436  fsumsplitsnun  11445  isumclim3  11449  isummulc2  11452  fsum2dlemstep  11460  fsumconst  11480  fsumabs  11491  fsumparts  11496  iserabs  11501  fsumiun  11503  isumshft  11516  cvgratnnlemseq  11552  mertenslemub  11560  mertenslemi1  11561  mertenslem2  11562  prod1dc  11612  fprodssdc  11616  fprodunsn  11630  fprodcl2lem  11631  fprodconst  11646  fprod2dlemstep  11648  fprodsplitsn  11659  eftlcl  11714  reeftlcl  11715  eftlub  11716  efsep  11717  effsumlt  11718  eirraplem  11802  2tp1odd  11907  bezoutlemstep  12016  alginv  12065  algfx  12070  cncongr1  12121  qnumdencoprm  12211  qeqnumdivden  12212  ctiunctal  12460  unct  12461  nninfdclemcl  12467  nninfdclemf  12468  nninfdclemp1  12469  nninfdc  12472  ressbasid  12548  ressressg  12553  prdsex  12740  imasex  12748  imasbas  12750  imasplusg  12751  imasmulr  12752  qusin  12769  issgrp  12832  sgrp1  12840  issgrpd  12841  ismndd  12864  mndprop  12868  ress0g  12870  insubm  12903  resmhm  12905  resmhm2  12906  resmhm2b  12907  grpprop  12929  grpsubfvalg  12955  grpressid  12971  grpsubpropdg  13014  imasgrp2  13018  imasgrp  13019  imasgrpf1  13020  mulgfvalg  13029  mulgpropdg  13070  subginv  13086  subgcl  13089  subgsub  13091  releqgg  13125  eqgex  13126  eqgfval  13127  qusgrp  13137  resghm  13160  ablprop  13197  subcmnd  13231  ablressid  13233  isrng  13249  isrngd  13268  rngressid  13269  imasrng  13271  issrg  13280  srgidmlem  13293  isring  13315  ringass  13331  ringidmlem  13337  ringabl  13347  ringprop  13355  isringd  13356  ring1  13372  ringressid  13374  imasring  13375  opprrng  13388  opprring  13390  opprringbg  13391  opprsubgg  13395  mulgass3  13396  dvdsrcld  13408  dvdsrex  13409  dvdsrcl2  13410  dvdsrid  13411  dvdsrtr  13412  dvdsrneg  13414  dvdsr01  13415  1unit  13418  unitcld  13419  opprunitd  13421  crngunit  13422  unitmulcl  13424  unitgrpbasd  13426  unitgrp  13427  unitabl  13428  unitgrpid  13429  unitsubm  13430  unitlinv  13437  unitrinv  13438  unitnegcl  13441  dvrfvald  13444  dvrvald  13445  dvrcl  13446  unitdvcl  13447  dvrid  13448  dvr1  13449  dvrdir  13454  rdivmuldivd  13455  dvdsrpropdg  13458  unitpropdg  13459  invrpropdg  13460  rhmf1o  13479  rhmdvdsr  13486  elrhmunit  13488  rhmunitinv  13489  issubrng2  13518  subrngpropd  13524  subrgcrng  13533  subrgdvds  13543  subrguss  13544  subrginv  13545  subrgdv  13546  subrgunit  13547  subrgugrp  13548  issubrg2  13549  subrgpropd  13556  aprirr  13560  aprsym  13561  aprcotr  13562  aprap  13563  islmodd  13570  lmodabl  13611  lss1  13639  lsssn0  13647  islss3  13656  lss1d  13660  lssintclm  13661  lsslsp  13706  sralmod  13727  sralmod0g  13728  rlmfn  13730  rlmvalg  13731  rlm0g  13734  rlmvnegg  13742  lidlssbas  13754  islidlm  13756  rnglidlmsgrp  13774  rnglidlrng  13775  qus2idrng  13801  crngridl  13805  quscrng  13808  dvdsrzring  13863  epttop  13974  lmss  14130  txlm  14163  lmcn2  14164  cnmpt2c  14174  txswaphmeolem  14204  blfvalps  14269  bdxmet  14385  fsumcncntop  14440  cncfmptc  14466  cncfmpt1f  14468  cdivcncfap  14471  negfcncf  14473  dvidlemap  14544  dvcnp2cntop  14547  dvaddxxbr  14549  dvmulxxbr  14550  dviaddf  14553  dvexp  14559  dvmptaddx  14565  dvmptmulx  14566  dvef  14572  sincn  14574  coscn  14575  lgsdir2lem5  14817  lgseisenlem2  14835  2lgsoddprmlem4  14844  2sqlem8  14854  nninfsellemeqinf  15150  nninffeq  15154  exmidsbthrlem  15155  cvgcmp2nlemabs  15165