Theorem eqidd 2232

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

Syntax hints:   → wi 4   = wceq 1398

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 1498  ax-ext 2213

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

This theorem is referenced by:  cbvraldva  2777  cbvrexdva  2778  rspcedeq1vd  2920  rspcedeq2vd  2921  nelrdva  3014  opeq2  3868  mpteq1  4178  tfisi  4691  feq23d  5485  f10d  5628  fvmptdv2  5745  elrnrexdm  5794  fmptco  5821  cofmpt  5824  ftpg  5846  fliftfun  5947  fliftval  5951  cbvmpo  6110  fconstmpo  6126  eqfnov2  6139  ovmpod  6159  ovmpodv2  6165  fvmpopr2d  6168  elovmporab  6232  elovmporab1w  6233  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  suppssof1  6262  ofco  6263  caofref  6269  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  caofrss  6276  caoftrn  6277  uchoice  6309  suppofss1dcl  6442  suppofss2dcl  6443  rdgivallem  6590  iserd  6771  ixpsnf1o  6948  modom  7037  1domsn  7044  mapxpen  7077  infnninf  7366  ctssexmid  7392  nninfdcinf  7413  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemginf  7418  nninfinfwlpo  7422  ofnegsub  9185  infrenegsupex  9871  fz0to4untppr  10402  fzo0to3tp  10508  modqsubmod  10688  0tonninf  10746  iseqovex  10764  seqvalcd  10767  seq3f1olemqsumkj  10817  seq3id  10831  seq3id2  10832  ccatws1ls  11266  pfxsuffeqwrdeq  11326  wrdind  11350  wrd2ind  11351  ccats1pfxeqbi  11370  s3eq2  11405  resqrexlemp1rp  11627  resqrexlemfp1  11630  resqrex  11647  infxrnegsupex  11884  climcl  11903  clim2  11904  climuni  11914  climeq  11920  2clim  11922  climshftlemg  11923  climabs0  11928  climcn1  11929  climcn2  11930  climge0  11946  climsqz  11956  climsqz2  11957  climcau  11968  climrecvg1n  11969  climcaucn  11972  serf0  11973  fzf1o  11997  isumz  12011  fisumss  12014  fsumsplitsn  12032  fsumsplitsnun  12041  isumclim3  12045  isummulc2  12048  fsum2dlemstep  12056  fsumconst  12076  fsumabs  12087  fsumparts  12092  iserabs  12097  fsumiun  12099  isumshft  12112  cvgratnnlemseq  12148  mertenslemub  12156  mertenslemi1  12157  mertenslem2  12158  prod1dc  12208  fprodssdc  12212  fprodunsn  12226  fprodcl2lem  12227  fprodconst  12242  fprod2dlemstep  12244  fprodsplitsn  12255  eftlcl  12310  reeftlcl  12311  eftlub  12312  efsep  12313  effsumlt  12314  eirraplem  12399  2tp1odd  12506  bezoutlemstep  12629  nninfctlemfo  12672  alginv  12680  algfx  12685  cncongr1  12736  qnumdencoprm  12826  qeqnumdivden  12827  ctiunctal  13123  unct  13124  nninfdclemcl  13130  nninfdclemf  13131  nninfdclemp1  13132  nninfdc  13135  ressbasid  13214  ressressg  13219  prdsex  13413  prdsbaslemss  13418  prdssca  13419  prdsbas  13420  prdsplusg  13421  prdsmulr  13422  imasex  13449  imasbas  13451  imasplusg  13452  imasmulr  13453  qusin  13470  igsumvalx  13533  gsumfzval  13535  gsumpropd  13536  gsumpropd2  13537  gsum0g  13540  gsumval2  13541  issgrp  13547  sgrp1  13555  issgrpd  13556  prdssgrpd  13559  ismndd  13581  mndprop  13585  ress0g  13587  prdsmndd  13592  imasmnd2  13596  insubm  13629  resmhm  13631  resmhm2  13632  resmhm2b  13633  gsumfzz  13639  grpprop  13662  grpsubfvalg  13689  grpressid  13705  grpsubpropdg  13748  prdsgrpd  13753  imasgrp2  13758  imasgrp  13759  imasgrpf1  13760  mulgfvalg  13769  mulgnngsum  13775  mulgpropdg  13812  submmulg  13814  subginv  13829  subgcl  13832  subgsub  13834  releqgg  13868  eqgex  13869  eqgfval  13870  qusgrp  13880  resghm  13908  ablprop  13945  subcmnd  13981  ablressid  13983  gsumfzmptfidmadd  13987  gsumfzconst  13989  gsumfzconstf  13990  gsumfzmhm2  13992  gsumsplit0  13994  isrng  14009  isrngd  14028  rngressid  14029  imasrng  14031  issrg  14040  srgidmlem  14053  isring  14075  ringass  14091  ringidmlem  14097  ringabl  14107  ringprop  14115  isringd  14116  ring1  14134  ringressid  14138  imasring  14139  opprrng  14152  opprring  14154  opprringbg  14155  opprsubgg  14159  mulgass3  14160  dvdsrcld  14173  dvdsrex  14174  dvdsrcl2  14175  dvdsrid  14176  dvdsrtr  14177  dvdsrneg  14179  dvdsr01  14180  1unit  14183  unitcld  14184  opprunitd  14186  crngunit  14187  unitmulcl  14189  unitgrpbasd  14191  unitgrp  14192  unitabl  14193  unitgrpid  14194  unitsubm  14195  unitlinv  14202  unitrinv  14203  unitnegcl  14206  dvrfvald  14209  dvrvald  14210  dvrcl  14211  unitdvcl  14212  dvrid  14213  dvr1  14214  dvrdir  14219  rdivmuldivd  14220  dvdsrpropdg  14223  unitpropdg  14224  invrpropdg  14225  rhmf1o  14244  rhmdvdsr  14251  elrhmunit  14253  rhmunitinv  14254  issubrng2  14286  subrngpropd  14292  subrgcrng  14301  subrgdvds  14311  subrguss  14312  subrginv  14313  subrgdv  14314  subrgunit  14315  subrgugrp  14316  issubrg2  14317  subrgpropd  14329  aprirr  14359  aprsym  14360  aprcotr  14361  aprap  14362  islmodd  14369  lmodabl  14410  lss1  14438  lsssn0  14446  islss3  14455  lss1d  14459  lssintclm  14460  lsslsp  14505  sralmod  14526  sralmod0g  14527  rlmfn  14529  rlmvalg  14530  rlm0g  14533  rlmvnegg  14541  lidlssbas  14553  islidlm  14555  rnglidlmsgrp  14573  rnglidlrng  14574  qus2idrng  14601  crngridl  14606  quscrng  14609  cnfldui  14665  dvdsrzring  14679  zrhpropd  14702  znzrh  14719  znbas  14720  zncrng  14721  znzrhfo  14724  znf1o  14727  znunit  14735  psrval  14742  psrbaglesuppg  14748  psrbagcon  14752  psrbagconf1o  14754  psrbasg  14755  psrplusgg  14759  mplsubgfilemcl  14780  mplplusgg  14784  epttop  14881  lmss  15037  txlm  15070  lmcn2  15071  cnmpt2c  15081  txswaphmeolem  15111  blfvalps  15176  bdxmet  15292  mpomulcn  15357  fsumcncntop  15358  cncfmptc  15387  cncfmpt1f  15389  cdivcncfap  15395  negfcncf  15397  divcncfap  15405  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvcnp2cntop  15490  dvaddxxbr  15492  dvmulxxbr  15493  dviaddf  15496  dvexp  15502  dvmptaddx  15510  dvmptmulx  15511  dvmptfsum  15516  dvef  15518  elply2  15526  elplyr  15531  plyaddlem1  15538  plycolemc  15549  sincn  15560  coscn  15561  lgsdir2lem5  15831  gausslemma2dlem1  15860  lgseisenlem2  15870  lgseisenlem3  15871  lgseisenlem4  15872  lgsquad2lem2  15881  2lgslem1b  15888  2lgslem3b1  15897  2lgslem3c1  15898  2lgsoddprmlem4  15911  2sqlem8  15922  usgredg4  16136  ushgredgedg  16147  ushgredgedgloop  16149  usgrstrrepeen  16152  uspgr1edc  16161  wlk1walkdom  16280  uspgr2wlkeq  16286  uspgr2wlkeqi  16288  clwwlknonmpo  16349  iseupth  16368  eupth2lem2dc  16380  konigsberglem2  16410  konigsberglem3  16411  nninfsellemeqinf  16722  nninffeq  16726  nnnninfex  16728  exmidsbthrlem  16730  cvgcmp2nlemabs  16744  gfsumval  16789  gsumgfsumlem  16792  gsumgfsum  16793  gfsumsn  16794