Theorem eqidd 2230

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

Syntax hints:   → wi 4   = wceq 1395

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 1495  ax-ext 2211

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

This theorem is referenced by:  cbvraldva  2774  cbvrexdva  2775  rspcedeq1vd  2917  rspcedeq2vd  2918  nelrdva  3011  opeq2  3861  mpteq1  4171  tfisi  4683  feq23d  5475  f10d  5615  fvmptdv2  5732  elrnrexdm  5782  fmptco  5809  cofmpt  5812  ftpg  5833  fliftfun  5932  fliftval  5936  cbvmpo  6095  fconstmpo  6111  eqfnov2  6124  ovmpod  6144  ovmpodv2  6150  fvmpopr2d  6153  elovmporab  6217  elovmporab1w  6218  ofvalg  6240  ofrval  6241  off  6243  ofres  6245  suppssof1  6248  ofco  6249  caofref  6255  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  caofrss  6262  caoftrn  6263  uchoice  6295  rdgivallem  6542  iserd  6723  ixpsnf1o  6900  modom  6989  1domsn  6996  mapxpen  7029  infnninf  7317  ctssexmid  7343  nninfdcinf  7364  nninfwlporlemd  7365  nninfwlporlem  7366  nninfwlpoimlemginf  7369  nninfinfwlpo  7373  ofnegsub  9135  infrenegsupex  9821  fz0to4untppr  10352  fzo0to3tp  10457  modqsubmod  10637  0tonninf  10695  iseqovex  10713  seqvalcd  10716  seq3f1olemqsumkj  10766  seq3id  10780  seq3id2  10781  ccatws1ls  11212  pfxsuffeqwrdeq  11272  wrdind  11296  wrd2ind  11297  ccats1pfxeqbi  11316  s3eq2  11351  resqrexlemp1rp  11560  resqrexlemfp1  11563  resqrex  11580  infxrnegsupex  11817  climcl  11836  clim2  11837  climuni  11847  climeq  11853  2clim  11855  climshftlemg  11856  climabs0  11861  climcn1  11862  climcn2  11863  climge0  11879  climsqz  11889  climsqz2  11890  climcau  11901  climrecvg1n  11902  climcaucn  11905  serf0  11906  isumz  11943  fisumss  11946  fsumsplitsn  11964  fsumsplitsnun  11973  isumclim3  11977  isummulc2  11980  fsum2dlemstep  11988  fsumconst  12008  fsumabs  12019  fsumparts  12024  iserabs  12029  fsumiun  12031  isumshft  12044  cvgratnnlemseq  12080  mertenslemub  12088  mertenslemi1  12089  mertenslem2  12090  prod1dc  12140  fprodssdc  12144  fprodunsn  12158  fprodcl2lem  12159  fprodconst  12174  fprod2dlemstep  12176  fprodsplitsn  12187  eftlcl  12242  reeftlcl  12243  eftlub  12244  efsep  12245  effsumlt  12246  eirraplem  12331  2tp1odd  12438  bezoutlemstep  12561  nninfctlemfo  12604  alginv  12612  algfx  12617  cncongr1  12668  qnumdencoprm  12758  qeqnumdivden  12759  ctiunctal  13055  unct  13056  nninfdclemcl  13062  nninfdclemf  13063  nninfdclemp1  13064  nninfdc  13067  ressbasid  13146  ressressg  13151  prdsex  13345  prdsbaslemss  13350  prdssca  13351  prdsbas  13352  prdsplusg  13353  prdsmulr  13354  imasex  13381  imasbas  13383  imasplusg  13384  imasmulr  13385  qusin  13402  igsumvalx  13465  gsumfzval  13467  gsumpropd  13468  gsumpropd2  13469  gsum0g  13472  gsumval2  13473  issgrp  13479  sgrp1  13487  issgrpd  13488  prdssgrpd  13491  ismndd  13513  mndprop  13517  ress0g  13519  prdsmndd  13524  imasmnd2  13528  insubm  13561  resmhm  13563  resmhm2  13564  resmhm2b  13565  gsumfzz  13571  grpprop  13594  grpsubfvalg  13621  grpressid  13637  grpsubpropdg  13680  prdsgrpd  13685  imasgrp2  13690  imasgrp  13691  imasgrpf1  13692  mulgfvalg  13701  mulgnngsum  13707  mulgpropdg  13744  submmulg  13746  subginv  13761  subgcl  13764  subgsub  13766  releqgg  13800  eqgex  13801  eqgfval  13802  qusgrp  13812  resghm  13840  ablprop  13877  subcmnd  13913  ablressid  13915  gsumfzmptfidmadd  13919  gsumfzconst  13921  gsumfzconstf  13922  gsumfzmhm2  13924  isrng  13940  isrngd  13959  rngressid  13960  imasrng  13962  issrg  13971  srgidmlem  13984  isring  14006  ringass  14022  ringidmlem  14028  ringabl  14038  ringprop  14046  isringd  14047  ring1  14065  ringressid  14069  imasring  14070  opprrng  14083  opprring  14085  opprringbg  14086  opprsubgg  14090  mulgass3  14091  dvdsrcld  14104  dvdsrex  14105  dvdsrcl2  14106  dvdsrid  14107  dvdsrtr  14108  dvdsrneg  14110  dvdsr01  14111  1unit  14114  unitcld  14115  opprunitd  14117  crngunit  14118  unitmulcl  14120  unitgrpbasd  14122  unitgrp  14123  unitabl  14124  unitgrpid  14125  unitsubm  14126  unitlinv  14133  unitrinv  14134  unitnegcl  14137  dvrfvald  14140  dvrvald  14141  dvrcl  14142  unitdvcl  14143  dvrid  14144  dvr1  14145  dvrdir  14150  rdivmuldivd  14151  dvdsrpropdg  14154  unitpropdg  14155  invrpropdg  14156  rhmf1o  14175  rhmdvdsr  14182  elrhmunit  14184  rhmunitinv  14185  issubrng2  14217  subrngpropd  14223  subrgcrng  14232  subrgdvds  14242  subrguss  14243  subrginv  14244  subrgdv  14245  subrgunit  14246  subrgugrp  14247  issubrg2  14248  subrgpropd  14260  aprirr  14290  aprsym  14291  aprcotr  14292  aprap  14293  islmodd  14300  lmodabl  14341  lss1  14369  lsssn0  14377  islss3  14386  lss1d  14390  lssintclm  14391  lsslsp  14436  sralmod  14457  sralmod0g  14458  rlmfn  14460  rlmvalg  14461  rlm0g  14464  rlmvnegg  14472  lidlssbas  14484  islidlm  14486  rnglidlmsgrp  14504  rnglidlrng  14505  qus2idrng  14532  crngridl  14537  quscrng  14540  cnfldui  14596  dvdsrzring  14610  zrhpropd  14633  znzrh  14650  znbas  14651  zncrng  14652  znzrhfo  14655  znf1o  14658  znunit  14666  psrval  14673  psrbaglesuppg  14679  psrbasg  14681  psrplusgg  14685  mplsubgfilemcl  14706  mplplusgg  14710  epttop  14807  lmss  14963  txlm  14996  lmcn2  14997  cnmpt2c  15007  txswaphmeolem  15037  blfvalps  15102  bdxmet  15218  mpomulcn  15283  fsumcncntop  15284  cncfmptc  15313  cncfmpt1f  15315  cdivcncfap  15321  negfcncf  15323  divcncfap  15331  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dviaddf  15422  dvexp  15428  dvmptaddx  15436  dvmptmulx  15437  dvmptfsum  15442  dvef  15444  elply2  15452  elplyr  15457  plyaddlem1  15464  plycolemc  15475  sincn  15486  coscn  15487  lgsdir2lem5  15754  gausslemma2dlem1  15783  lgseisenlem2  15793  lgseisenlem3  15794  lgseisenlem4  15795  lgsquad2lem2  15804  2lgslem1b  15811  2lgslem3b1  15820  2lgslem3c1  15821  2lgsoddprmlem4  15834  2sqlem8  15845  usgredg4  16059  ushgredgedg  16070  ushgredgedgloop  16072  usgrstrrepeen  16075  uspgr1edc  16084  wlk1walkdom  16170  uspgr2wlkeq  16176  uspgr2wlkeqi  16178  clwwlknonmpo  16237  iseupth  16256  nninfsellemeqinf  16568  nninffeq  16572  nnnninfex  16574  exmidsbthrlem  16576  cvgcmp2nlemabs  16586  gfsumval  16630  gsumgfsumlem  16633  gsumgfsum  16634