Theorem eqidd 2239

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cbvraldva  2795  cbvrexdva  2796  rspcedeq1vd  2939  rspcedeq2vd  2940  nelrdva  3033  opeq2  3905  mpteq1  4216  mpteq1i  4218  tfisi  4736  feq23d  5532  f10d  5678  fvmptdv2  5798  elrnrexdm  5850  fmptco  5877  cofmpt  5880  ftpg  5902  fliftfun  6005  fliftval  6009  cbvmpo  6170  fconstmpo  6186  eqfnov2  6199  ovmpod  6219  ovmpodv2  6225  fvmpopr2d  6228  elovmporab  6292  elovmporab1w  6293  ofvalg  6316  ofrval  6317  off  6319  ofres  6321  suppssof1  6324  ofco  6325  caofref  6331  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  caofrss  6338  caoftrn  6339  uchoice  6375  suppofss1dcl  6508  suppofss2dcl  6509  rdgivallem  6657  iserd  6838  ixpsnf1o  7024  modom  7114  1domsn  7121  mapxpen  7154  ofrfidc  7323  infnninf  7470  ctssexmid  7496  nninfdcinf  7517  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemginf  7522  nninfinfwlpo  7526  ofsubeq0  9300  ofnegsub  9301  infrenegsupex  10009  fz0to4untppr  10547  fzo0to3tp  10653  modqsubmod  10839  0tonninf  10897  iseqovex  10915  seqvalcd  10918  seq3f1olemqsumkj  10968  seq3id  10982  seq3id2  10983  ccatws1ls  11431  pfxsuffeqwrdeq  11491  wrdind  11515  wrd2ind  11516  ccats1pfxeqbi  11535  s3eq2  11570  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrex  11813  infxrnegsupex  12053  climcl  12072  clim2  12073  climuni  12083  climeq  12089  2clim  12091  climshftlemg  12092  climabs0  12097  climcn1  12098  climcn2  12099  climge0  12115  climsqz  12125  climsqz2  12126  climcau  12137  climrecvg1n  12138  climcaucn  12141  serf0  12142  fzf1o  12166  isumz  12180  fisumss  12183  fsumsplitsn  12201  fsumsplitsnun  12210  isumclim3  12214  isummulc2  12217  fsum2dlemstep  12225  fsumconst  12245  fsumabs  12256  fsumparts  12261  iserabs  12266  fsumiun  12268  isumshft  12281  cvgratnnlemseq  12317  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  prod1dc  12377  fprodssdc  12381  fprodunsn  12395  fprodcl2lem  12396  fprodconst  12411  fprod2dlemstep  12413  fprodsplitsn  12424  eftlcl  12479  reeftlcl  12480  eftlub  12481  efsep  12482  effsumlt  12483  eirraplem  12568  2tp1odd  12675  bezoutlemstep  12798  nninfctlemfo  12841  alginv  12849  algfx  12854  cncongr1  12905  qnumdencoprm  12997  qeqnumdivden  12998  ballotfilemgun  13325  ballotfilemfg  13326  ballotfilemfrc  13327  ctiunctal  13389  unct  13390  nninfdclemcl  13396  nninfdclemf  13397  nninfdclemp1  13398  nninfdc  13401  ressbasid  13482  ressressg  13487  imasex  13684  imasbas  13686  imasplusg  13687  imasmulr  13688  qusin  13705  gzsumvalx  13767  gzsumfzval  13769  gzsum0  13771  gzsumval2  13772  issgrp  13776  sgrp1  13784  issgrpd  13785  ismndd  13808  mndprop  13812  ress0g  13814  imasmnd2  13817  insubm  13850  resmhm  13852  resmhm2  13853  resmhm2b  13854  grpprop  13881  grpsubfvalg  13908  grpressid  13924  grpsubpropdg  13967  imasgrp2  13971  imasgrp  13972  imasgrpf1  13973  mulgfvalg  13982  mulgnngzsum  13988  mulgpropdg  14025  submmulg  14027  subginv  14042  subgcl  14045  subgsub  14047  releqgg  14081  eqgex  14082  eqgfval  14083  qusgrp  14093  resghm  14121  resscntz  14165  ablprop  14189  cmnsubm  14201  subcmnd  14226  ablressid  14228  gzsumconst  14232  gzsumconstf  14233  gzsummhm2  14235  gzsumsplit0  14237  gzsumshift  14238  gsumvalfi  14241  gzsumgsum  14244  gsumsncmn  14245  gsumzfi  14247  gsumunsnfd  14258  gsummhm2fi  14264  gsum2dfilem2  14271  gsumcom2fi  14274  prdsex  14278  prdsbaslemss  14280  prdssca  14281  prdsbas  14282  prdsplusg  14283  prdsmulr  14284  prdssgrpd  14297  prdsmndd  14300  prdsgrpd  14303  isrng  14339  isrngd  14358  rngressid  14359  imasrng  14361  issrg  14375  srgidmlem  14388  isring  14410  ringass  14426  ringidmlem  14433  ringabl  14443  ringprop  14451  isringd  14452  ring1  14470  ringressid  14476  imasring  14477  opprrng  14490  opprring  14492  opprringbg  14493  opprsubgg  14498  mulgass3  14499  dvdsrcld  14512  dvdsrex  14513  dvdsrcl2  14514  dvdsrid  14515  dvdsrtr  14516  dvdsrneg  14518  dvdsr01  14519  1unit  14522  unitcld  14523  opprunitd  14525  crngunit  14526  unitmulcl  14528  unitgrpbasd  14530  unitgrp  14531  unitabl  14532  unitgrpid  14533  unitsubm  14534  unitlinv  14541  unitrinv  14542  unitnegcl  14545  dvrfvald  14548  dvrvald  14549  dvrcl  14550  unitdvcl  14551  dvrid  14552  dvr1  14553  dvrdir  14558  rdivmuldivd  14559  dvdsrpropdg  14562  unitpropdg  14563  invrpropdg  14564  rhmf1o  14583  rhmdvdsr  14590  elrhmunit  14592  rhmunitinv  14593  opprlring  14612  issubrng2  14626  subrngpropd  14632  subrgcrng  14641  subrgdvds  14651  subrguss  14652  subrginv  14653  subrgdv  14654  subrgunit  14655  subrgugrp  14656  issubrg2  14657  subrgpropd  14669  aprunit  14700  aprirr  14703  aprsym  14704  aprcotr  14705  aprap  14706  aprnzr  14707  aprlring  14708  aprprop  14709  opprdrng  14728  islmodd  14737  lmodabl  14779  lss1  14807  lsssn0  14815  islss3  14824  lss1d  14828  lssintclm  14829  lsslsp  14874  sralmod  14895  sralmod0g  14896  rlmfn  14898  rlmvalg  14899  rlm0g  14902  rlmvnegg  14910  lidlssbas  14922  islidlm  14924  rnglidlmsgrp  14942  rnglidlrng  14943  qus2idrng  14970  crngridl  14975  quscrng  14978  cnfldui  15032  dvdsrzring  15046  zrhpropd  15069  znzrh  15086  znbas  15087  zncrng  15088  znzrhfo  15091  znf1o  15094  znunit  15102  isassad  15119  issubassa3  15120  asclfval  15129  ressascl  15147  psrval  15160  psrbaglesuppg  15170  psrbagcon  15174  psrbaglefifi  15175  psrbagconf1o  15177  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  psrass1filem  15186  psrbasg  15187  psrplusgg  15191  psrmulrg  15195  psrlidmfi  15208  psrdifi  15211  psrdirfi  15212  psrringfi  15213  mplsubgfilemcl  15232  mplplusgg  15236  epttop  15333  lmss  15489  txlm  15522  lmcn2  15523  cnmpt2c  15533  txswaphmeolem  15563  blfvalps  15628  bdxmet  15744  mpomulcn  15809  fsumcncntop  15810  cncfmptc  15839  cncfmpt1f  15841  cdivcncfap  15847  negfcncf  15849  divcncfap  15857  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dviaddf  15948  dvexp  15954  dvmptaddx  15962  dvmptmulx  15963  dvmptfsum  15968  dvef  15970  elply2  15978  elplyr  15983  plyaddlem1  15990  plycolemc  16001  sincn  16012  coscn  16013  logfac  16143  chtublem  16312  bposlem6  16333  lgsdir2lem5  16373  gausslemma2dlem1  16402  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquad2lem2  16423  2lgslem1b  16430  2lgslem3b1  16439  2lgslem3c1  16440  2lgsoddprmlem4  16453  2sqlem8  16464  usgredg4  16678  ushgredgedg  16689  ushgredgedgloop  16691  usgrstrrepeen  16694  uspgr1edc  16703  wlk1walkdom  16822  uspgr2wlkeq  16828  uspgr2wlkeqi  16830  clwwlknonmpo  16891  iseupth  16910  eupth2lem2dc  16922  konigsberglem2  16952  konigsberglem3  16953  nninfsellemeqinf  17282  nninffeq  17286  nnnninfex  17288  exmidsbthrlem  17290  cvgcmp2nlemabs  17304