Theorem eqidd 2239

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	|- ( ph -> A = A )

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2238	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

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  4215  tfisi  4734  feq23d  5529  f10d  5675  fvmptdv2  5795  elrnrexdm  5847  fmptco  5874  cofmpt  5877  ftpg  5899  fliftfun  6002  fliftval  6006  cbvmpo  6167  fconstmpo  6183  eqfnov2  6196  ovmpod  6216  ovmpodv2  6222  fvmpopr2d  6225  elovmporab  6289  elovmporab1w  6290  ofvalg  6312  ofrval  6313  off  6315  ofres  6317  suppssof1  6320  ofco  6321  caofref  6327  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  caofrss  6334  caoftrn  6335  uchoice  6371  suppofss1dcl  6504  suppofss2dcl  6505  rdgivallem  6652  iserd  6833  ixpsnf1o  7018  modom  7108  1domsn  7115  mapxpen  7148  infnninf  7464  ctssexmid  7490  nninfdcinf  7511  nninfwlporlemd  7512  nninfwlporlem  7513  nninfwlpoimlemginf  7516  nninfinfwlpo  7520  ofnegsub  9294  infrenegsupex  10003  fz0to4untppr  10541  fzo0to3tp  10647  modqsubmod  10832  0tonninf  10890  iseqovex  10908  seqvalcd  10911  seq3f1olemqsumkj  10961  seq3id  10975  seq3id2  10976  ccatws1ls  11424  pfxsuffeqwrdeq  11484  wrdind  11508  wrd2ind  11509  ccats1pfxeqbi  11528  s3eq2  11563  resqrexlemp1rp  11786  resqrexlemfp1  11789  resqrex  11806  infxrnegsupex  12045  climcl  12064  clim2  12065  climuni  12075  climeq  12081  2clim  12083  climshftlemg  12084  climabs0  12089  climcn1  12090  climcn2  12091  climge0  12107  climsqz  12117  climsqz2  12118  climcau  12129  climrecvg1n  12130  climcaucn  12133  serf0  12134  fzf1o  12158  isumz  12172  fisumss  12175  fsumsplitsn  12193  fsumsplitsnun  12202  isumclim3  12206  isummulc2  12209  fsum2dlemstep  12217  fsumconst  12237  fsumabs  12248  fsumparts  12253  iserabs  12258  fsumiun  12260  isumshft  12273  cvgratnnlemseq  12309  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  prod1dc  12369  fprodssdc  12373  fprodunsn  12387  fprodcl2lem  12388  fprodconst  12403  fprod2dlemstep  12405  fprodsplitsn  12416  eftlcl  12471  reeftlcl  12472  eftlub  12473  efsep  12474  effsumlt  12475  eirraplem  12560  2tp1odd  12667  bezoutlemstep  12790  nninfctlemfo  12833  alginv  12841  algfx  12846  cncongr1  12897  qnumdencoprm  12989  qeqnumdivden  12990  ballotfilemgun  13317  ballotfilemfg  13318  ballotfilemfrc  13319  ctiunctal  13381  unct  13382  nninfdclemcl  13388  nninfdclemf  13389  nninfdclemp1  13390  nninfdc  13393  ressbasid  13473  ressressg  13478  imasex  13675  imasbas  13677  imasplusg  13678  imasmulr  13679  qusin  13696  gzsumvalx  13758  gzsumfzval  13760  gzsum0  13762  gzsumval2  13763  issgrp  13767  sgrp1  13775  issgrpd  13776  ismndd  13799  mndprop  13803  ress0g  13805  imasmnd2  13808  insubm  13841  resmhm  13843  resmhm2  13844  resmhm2b  13845  grpprop  13872  grpsubfvalg  13899  grpressid  13915  grpsubpropdg  13958  imasgrp2  13962  imasgrp  13963  imasgrpf1  13964  mulgfvalg  13973  mulgnngzsum  13979  mulgpropdg  14016  submmulg  14018  subginv  14033  subgcl  14036  subgsub  14038  releqgg  14072  eqgex  14073  eqgfval  14074  qusgrp  14084  resghm  14112  ablprop  14149  cmnsubm  14161  subcmnd  14186  ablressid  14188  gzsumconst  14192  gzsumconstf  14193  gzsummhm2  14195  gzsumsplit0  14197  gzsumshift  14198  gsumvalfi  14201  gzsumgsum  14204  gsumsncmn  14205  gsumzfi  14207  gsummhm2fi  14214  prdsex  14221  prdsbaslemss  14223  prdssca  14224  prdsbas  14225  prdsplusg  14226  prdsmulr  14227  prdssgrpd  14240  prdsmndd  14243  prdsgrpd  14246  isrng  14282  isrngd  14301  rngressid  14302  imasrng  14304  issrg  14318  srgidmlem  14331  isring  14353  ringass  14369  ringidmlem  14376  ringabl  14386  ringprop  14394  isringd  14395  ring1  14413  ringressid  14417  imasring  14418  opprrng  14431  opprring  14433  opprringbg  14434  opprsubgg  14439  mulgass3  14440  dvdsrcld  14453  dvdsrex  14454  dvdsrcl2  14455  dvdsrid  14456  dvdsrtr  14457  dvdsrneg  14459  dvdsr01  14460  1unit  14463  unitcld  14464  opprunitd  14466  crngunit  14467  unitmulcl  14469  unitgrpbasd  14471  unitgrp  14472  unitabl  14473  unitgrpid  14474  unitsubm  14475  unitlinv  14482  unitrinv  14483  unitnegcl  14486  dvrfvald  14489  dvrvald  14490  dvrcl  14491  unitdvcl  14492  dvrid  14493  dvr1  14494  dvrdir  14499  rdivmuldivd  14500  dvdsrpropdg  14503  unitpropdg  14504  invrpropdg  14505  rhmf1o  14524  rhmdvdsr  14531  elrhmunit  14533  rhmunitinv  14534  opprlring  14553  issubrng2  14567  subrngpropd  14573  subrgcrng  14582  subrgdvds  14592  subrguss  14593  subrginv  14594  subrgdv  14595  subrgunit  14596  subrgugrp  14597  issubrg2  14598  subrgpropd  14610  aprunit  14641  aprirr  14644  aprsym  14645  aprcotr  14646  aprap  14647  aprnzr  14648  aprlring  14649  aprprop  14650  opprdrng  14669  islmodd  14678  lmodabl  14720  lss1  14748  lsssn0  14756  islss3  14765  lss1d  14769  lssintclm  14770  lsslsp  14815  sralmod  14836  sralmod0g  14837  rlmfn  14839  rlmvalg  14840  rlm0g  14843  rlmvnegg  14851  lidlssbas  14863  islidlm  14865  rnglidlmsgrp  14883  rnglidlrng  14884  qus2idrng  14911  crngridl  14916  quscrng  14919  cnfldui  14973  dvdsrzring  14987  zrhpropd  15010  znzrh  15027  znbas  15028  zncrng  15029  znzrhfo  15032  znf1o  15035  znunit  15043  isassad  15060  issubassa3  15061  asclfval  15070  ressascl  15088  psrval  15099  psrbaglesuppg  15106  psrbagcon  15111  psrbagconf1o  15113  psrbasg  15114  psrplusgg  15118  mplsubgfilemcl  15139  mplplusgg  15143  epttop  15240  lmss  15396  txlm  15429  lmcn2  15430  cnmpt2c  15440  txswaphmeolem  15470  blfvalps  15535  bdxmet  15651  mpomulcn  15716  fsumcncntop  15717  cncfmptc  15746  cncfmpt1f  15748  cdivcncfap  15754  negfcncf  15756  divcncfap  15764  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dviaddf  15855  dvexp  15861  dvmptaddx  15869  dvmptmulx  15870  dvmptfsum  15875  dvef  15877  elply2  15885  elplyr  15890  plyaddlem1  15897  plycolemc  15908  sincn  15919  coscn  15920  logfac  16048  lgsdir2lem5  16249  gausslemma2dlem1  16278  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquad2lem2  16299  2lgslem1b  16306  2lgslem3b1  16315  2lgslem3c1  16316  2lgsoddprmlem4  16329  2sqlem8  16340  usgredg4  16554  ushgredgedg  16565  ushgredgedgloop  16567  usgrstrrepeen  16570  uspgr1edc  16579  wlk1walkdom  16698  uspgr2wlkeq  16704  uspgr2wlkeqi  16706  clwwlknonmpo  16767  iseupth  16786  eupth2lem2dc  16798  konigsberglem2  16828  konigsberglem3  16829  nninfsellemeqinf  17157  nninffeq  17161  nnnninfex  17163  exmidsbthrlem  17165  cvgcmp2nlemabs  17179