Theorem eqidd 2235

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 2234	. 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 2216

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

This theorem is referenced by:  cbvraldva  2789  cbvrexdva  2790  rspcedeq1vd  2933  rspcedeq2vd  2934  nelrdva  3027  opeq2  3889  mpteq1  4199  tfisi  4714  feq23d  5509  f10d  5655  fvmptdv2  5772  elrnrexdm  5821  fmptco  5848  cofmpt  5851  ftpg  5873  fliftfun  5975  fliftval  5979  cbvmpo  6140  fconstmpo  6156  eqfnov2  6169  ovmpod  6189  ovmpodv2  6195  fvmpopr2d  6198  elovmporab  6262  elovmporab1w  6263  ofvalg  6285  ofrval  6286  off  6288  ofres  6290  suppssof1  6293  ofco  6294  caofref  6300  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  caofrss  6307  caoftrn  6308  uchoice  6344  suppofss1dcl  6477  suppofss2dcl  6478  rdgivallem  6625  iserd  6806  ixpsnf1o  6984  modom  7074  1domsn  7081  mapxpen  7114  infnninf  7428  ctssexmid  7454  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  nninfwlpoimlemginf  7480  nninfinfwlpo  7484  ofnegsub  9253  infrenegsupex  9944  fz0to4untppr  10480  fzo0to3tp  10586  modqsubmod  10768  0tonninf  10826  iseqovex  10844  seqvalcd  10847  seq3f1olemqsumkj  10897  seq3id  10911  seq3id2  10912  ccatws1ls  11355  pfxsuffeqwrdeq  11415  wrdind  11439  wrd2ind  11440  ccats1pfxeqbi  11459  s3eq2  11494  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrex  11736  infxrnegsupex  11973  climcl  11992  clim2  11993  climuni  12003  climeq  12009  2clim  12011  climshftlemg  12012  climabs0  12017  climcn1  12018  climcn2  12019  climge0  12035  climsqz  12045  climsqz2  12046  climcau  12057  climrecvg1n  12058  climcaucn  12061  serf0  12062  fzf1o  12086  isumz  12100  fisumss  12103  fsumsplitsn  12121  fsumsplitsnun  12130  isumclim3  12134  isummulc2  12137  fsum2dlemstep  12145  fsumconst  12165  fsumabs  12176  fsumparts  12181  iserabs  12186  fsumiun  12188  isumshft  12201  cvgratnnlemseq  12237  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  prod1dc  12297  fprodssdc  12301  fprodunsn  12315  fprodcl2lem  12316  fprodconst  12331  fprod2dlemstep  12333  fprodsplitsn  12344  eftlcl  12399  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  eirraplem  12488  2tp1odd  12595  bezoutlemstep  12718  nninfctlemfo  12761  alginv  12769  algfx  12774  cncongr1  12825  qnumdencoprm  12915  qeqnumdivden  12916  ballotfilemgun  13212  ballotfilemfg  13213  ballotfilemfrc  13214  ctiunctal  13276  unct  13277  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  nninfdc  13288  ressbasid  13367  ressressg  13372  prdsex  13566  prdsbaslemss  13571  prdssca  13572  prdsbas  13573  prdsplusg  13574  prdsmulr  13575  imasex  13602  imasbas  13604  imasplusg  13605  imasmulr  13606  qusin  13623  igsumvalx  13686  gsumfzval  13688  gsumpropd  13689  gsumpropd2  13690  gsum0g  13693  gsumval2  13694  issgrp  13700  sgrp1  13708  issgrpd  13709  prdssgrpd  13712  ismndd  13734  mndprop  13738  ress0g  13740  prdsmndd  13745  imasmnd2  13749  insubm  13782  resmhm  13784  resmhm2  13785  resmhm2b  13786  gsumfzz  13792  grpprop  13815  grpsubfvalg  13842  grpressid  13858  grpsubpropdg  13901  prdsgrpd  13906  imasgrp2  13911  imasgrp  13912  imasgrpf1  13913  mulgfvalg  13922  mulgnngsum  13928  mulgpropdg  13965  submmulg  13967  subginv  13982  subgcl  13985  subgsub  13987  releqgg  14021  eqgex  14022  eqgfval  14023  qusgrp  14033  resghm  14061  ablprop  14098  subcmnd  14134  ablressid  14136  gsumfzmptfidmadd  14140  gsumfzconst  14142  gsumfzconstf  14143  gsumfzmhm2  14145  gsumsplit0  14147  isrng  14162  isrngd  14181  rngressid  14182  imasrng  14184  issrg  14193  srgidmlem  14206  isring  14228  ringass  14244  ringidmlem  14250  ringabl  14260  ringprop  14268  isringd  14269  ring1  14287  ringressid  14291  imasring  14292  opprrng  14305  opprring  14307  opprringbg  14308  opprsubgg  14313  mulgass3  14314  dvdsrcld  14327  dvdsrex  14328  dvdsrcl2  14329  dvdsrid  14330  dvdsrtr  14331  dvdsrneg  14333  dvdsr01  14334  1unit  14337  unitcld  14338  opprunitd  14340  crngunit  14341  unitmulcl  14343  unitgrpbasd  14345  unitgrp  14346  unitabl  14347  unitgrpid  14348  unitsubm  14349  unitlinv  14356  unitrinv  14357  unitnegcl  14360  dvrfvald  14363  dvrvald  14364  dvrcl  14365  unitdvcl  14366  dvrid  14367  dvr1  14368  dvrdir  14373  rdivmuldivd  14374  dvdsrpropdg  14377  unitpropdg  14378  invrpropdg  14379  rhmf1o  14398  rhmdvdsr  14405  elrhmunit  14407  rhmunitinv  14408  opprlring  14427  issubrng2  14441  subrngpropd  14447  subrgcrng  14456  subrgdvds  14466  subrguss  14467  subrginv  14468  subrgdv  14469  subrgunit  14470  subrgugrp  14471  issubrg2  14472  subrgpropd  14484  aprunit  14515  aprirr  14518  aprsym  14519  aprcotr  14520  aprap  14521  aprnzr  14522  aprlring  14523  aprprop  14524  opprdrng  14543  islmodd  14553  lmodabl  14594  lss1  14622  lsssn0  14630  islss3  14639  lss1d  14643  lssintclm  14644  lsslsp  14689  sralmod  14710  sralmod0g  14711  rlmfn  14713  rlmvalg  14714  rlm0g  14717  rlmvnegg  14725  lidlssbas  14737  islidlm  14739  rnglidlmsgrp  14757  rnglidlrng  14758  qus2idrng  14785  crngridl  14790  quscrng  14793  cnfldui  14849  dvdsrzring  14863  zrhpropd  14886  znzrh  14903  znbas  14904  zncrng  14905  znzrhfo  14908  znf1o  14911  znunit  14919  psrval  14926  psrbaglesuppg  14933  psrbagcon  14938  psrbagconf1o  14940  psrbasg  14941  psrplusgg  14945  mplsubgfilemcl  14966  mplplusgg  14970  epttop  15067  lmss  15223  txlm  15256  lmcn2  15257  cnmpt2c  15267  txswaphmeolem  15297  blfvalps  15362  bdxmet  15478  mpomulcn  15543  fsumcncntop  15544  cncfmptc  15573  cncfmpt1f  15575  cdivcncfap  15581  negfcncf  15583  divcncfap  15591  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvcnp2cntop  15676  dvaddxxbr  15678  dvmulxxbr  15679  dviaddf  15682  dvexp  15688  dvmptaddx  15696  dvmptmulx  15697  dvmptfsum  15702  dvef  15704  elply2  15712  elplyr  15717  plyaddlem1  15724  plycolemc  15735  sincn  15746  coscn  15747  lgsdir2lem5  16017  gausslemma2dlem1  16046  lgseisenlem2  16056  lgseisenlem3  16057  lgseisenlem4  16058  lgsquad2lem2  16067  2lgslem1b  16074  2lgslem3b1  16083  2lgslem3c1  16084  2lgsoddprmlem4  16097  2sqlem8  16108  usgredg4  16322  ushgredgedg  16333  ushgredgedgloop  16335  usgrstrrepeen  16338  uspgr1edc  16347  wlk1walkdom  16466  uspgr2wlkeq  16472  uspgr2wlkeqi  16474  clwwlknonmpo  16535  iseupth  16554  eupth2lem2dc  16566  konigsberglem2  16596  konigsberglem3  16597  nninfsellemeqinf  16906  nninffeq  16910  nnnninfex  16912  exmidsbthrlem  16914  cvgcmp2nlemabs  16928  gfsumval  16974  gsumgfsumlem  16977  gsumgfsum  16978  gfsumsn  16979  gfsumz  16981