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  9292  infrenegsupex  9994  fz0to4untppr  10531  fzo0to3tp  10637  modqsubmod  10819  0tonninf  10877  iseqovex  10895  seqvalcd  10898  seq3f1olemqsumkj  10948  seq3id  10962  seq3id2  10963  ccatws1ls  11410  pfxsuffeqwrdeq  11470  wrdind  11494  wrd2ind  11495  ccats1pfxeqbi  11514  s3eq2  11549  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrex  11792  infxrnegsupex  12029  climcl  12048  clim2  12049  climuni  12059  climeq  12065  2clim  12067  climshftlemg  12068  climabs0  12073  climcn1  12074  climcn2  12075  climge0  12091  climsqz  12101  climsqz2  12102  climcau  12113  climrecvg1n  12114  climcaucn  12117  serf0  12118  fzf1o  12142  isumz  12156  fisumss  12159  fsumsplitsn  12177  fsumsplitsnun  12186  isumclim3  12190  isummulc2  12193  fsum2dlemstep  12201  fsumconst  12221  fsumabs  12232  fsumparts  12237  iserabs  12242  fsumiun  12244  isumshft  12257  cvgratnnlemseq  12293  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  prod1dc  12353  fprodssdc  12357  fprodunsn  12371  fprodcl2lem  12372  fprodconst  12387  fprod2dlemstep  12389  fprodsplitsn  12400  eftlcl  12455  reeftlcl  12456  eftlub  12457  efsep  12458  effsumlt  12459  eirraplem  12544  2tp1odd  12651  bezoutlemstep  12774  nninfctlemfo  12817  alginv  12825  algfx  12830  cncongr1  12881  qnumdencoprm  12971  qeqnumdivden  12972  ballotfilemgun  13268  ballotfilemfg  13269  ballotfilemfrc  13270  ctiunctal  13332  unct  13333  nninfdclemcl  13339  nninfdclemf  13340  nninfdclemp1  13341  nninfdc  13344  ressbasid  13424  ressressg  13429  imasex  13626  imasbas  13628  imasplusg  13629  imasmulr  13630  qusin  13647  gzsumvalx  13709  gzsumfzval  13711  gzsum0  13713  gzsumval2  13714  issgrp  13718  sgrp1  13726  issgrpd  13727  ismndd  13750  mndprop  13754  ress0g  13756  imasmnd2  13759  insubm  13792  resmhm  13794  resmhm2  13795  resmhm2b  13796  grpprop  13823  grpsubfvalg  13850  grpressid  13866  grpsubpropdg  13909  imasgrp2  13913  imasgrp  13914  imasgrpf1  13915  mulgfvalg  13924  mulgnngzsum  13930  mulgpropdg  13967  submmulg  13969  subginv  13984  subgcl  13987  subgsub  13989  releqgg  14023  eqgex  14024  eqgfval  14025  qusgrp  14035  resghm  14063  ablprop  14100  cmnsubm  14112  subcmnd  14137  ablressid  14139  gzsumconst  14143  gzsumconstf  14144  gzsummhm2  14146  gzsumsplit0  14148  gzsumshift  14149  gsumvalfi  14152  gzsumgsum  14155  gsumsncmn  14156  gsumzfi  14158  gsummhm2fi  14165  prdsex  14172  prdsbaslemss  14174  prdssca  14175  prdsbas  14176  prdsplusg  14177  prdsmulr  14178  prdssgrpd  14191  prdsmndd  14194  prdsgrpd  14197  isrng  14233  isrngd  14252  rngressid  14253  imasrng  14255  issrg  14269  srgidmlem  14282  isring  14304  ringass  14320  ringidmlem  14327  ringabl  14337  ringprop  14345  isringd  14346  ring1  14364  ringressid  14368  imasring  14369  opprrng  14382  opprring  14384  opprringbg  14385  opprsubgg  14390  mulgass3  14391  dvdsrcld  14404  dvdsrex  14405  dvdsrcl2  14406  dvdsrid  14407  dvdsrtr  14408  dvdsrneg  14410  dvdsr01  14411  1unit  14414  unitcld  14415  opprunitd  14417  crngunit  14418  unitmulcl  14420  unitgrpbasd  14422  unitgrp  14423  unitabl  14424  unitgrpid  14425  unitsubm  14426  unitlinv  14433  unitrinv  14434  unitnegcl  14437  dvrfvald  14440  dvrvald  14441  dvrcl  14442  unitdvcl  14443  dvrid  14444  dvr1  14445  dvrdir  14450  rdivmuldivd  14451  dvdsrpropdg  14454  unitpropdg  14455  invrpropdg  14456  rhmf1o  14475  rhmdvdsr  14482  elrhmunit  14484  rhmunitinv  14485  opprlring  14504  issubrng2  14518  subrngpropd  14524  subrgcrng  14533  subrgdvds  14543  subrguss  14544  subrginv  14545  subrgdv  14546  subrgunit  14547  subrgugrp  14548  issubrg2  14549  subrgpropd  14561  aprunit  14592  aprirr  14595  aprsym  14596  aprcotr  14597  aprap  14598  aprnzr  14599  aprlring  14600  aprprop  14601  opprdrng  14620  islmodd  14629  lmodabl  14671  lss1  14699  lsssn0  14707  islss3  14716  lss1d  14720  lssintclm  14721  lsslsp  14766  sralmod  14787  sralmod0g  14788  rlmfn  14790  rlmvalg  14791  rlm0g  14794  rlmvnegg  14802  lidlssbas  14814  islidlm  14816  rnglidlmsgrp  14834  rnglidlrng  14835  qus2idrng  14862  crngridl  14867  quscrng  14870  cnfldui  14924  dvdsrzring  14938  zrhpropd  14961  znzrh  14978  znbas  14979  zncrng  14980  znzrhfo  14983  znf1o  14986  znunit  14994  isassad  15011  issubassa3  15012  asclfval  15021  ressascl  15039  psrval  15050  psrbaglesuppg  15057  psrbagcon  15062  psrbagconf1o  15064  psrbasg  15065  psrplusgg  15069  mplsubgfilemcl  15090  mplplusgg  15094  epttop  15191  lmss  15347  txlm  15380  lmcn2  15381  cnmpt2c  15391  txswaphmeolem  15421  blfvalps  15486  bdxmet  15602  mpomulcn  15667  fsumcncntop  15668  cncfmptc  15697  cncfmpt1f  15699  cdivcncfap  15705  negfcncf  15707  divcncfap  15715  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dviaddf  15806  dvexp  15812  dvmptaddx  15820  dvmptmulx  15821  dvmptfsum  15826  dvef  15828  elply2  15836  elplyr  15841  plyaddlem1  15848  plycolemc  15859  sincn  15870  coscn  15871  logfac  15995  lgsdir2lem5  16151  gausslemma2dlem1  16180  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquad2lem2  16201  2lgslem1b  16208  2lgslem3b1  16217  2lgslem3c1  16218  2lgsoddprmlem4  16231  2sqlem8  16242  usgredg4  16456  ushgredgedg  16467  ushgredgedgloop  16469  usgrstrrepeen  16472  uspgr1edc  16481  wlk1walkdom  16600  uspgr2wlkeq  16606  uspgr2wlkeqi  16608  clwwlknonmpo  16669  iseupth  16688  eupth2lem2dc  16700  konigsberglem2  16730  konigsberglem3  16731  nninfsellemeqinf  17059  nninffeq  17063  nnnninfex  17065  exmidsbthrlem  17067  cvgcmp2nlemabs  17081