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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1502  ax-ext 2220

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

This theorem is referenced by:  cbvraldva  2795  cbvrexdva  2796  rspcedeq1vd  2939  rspcedeq2vd  2940  nelrdva  3033  opeq2  3900  mpteq1  4210  tfisi  4729  feq23d  5524  f10d  5670  fvmptdv2  5789  elrnrexdm  5838  fmptco  5865  cofmpt  5868  ftpg  5890  fliftfun  5992  fliftval  5996  cbvmpo  6157  fconstmpo  6173  eqfnov2  6186  ovmpod  6206  ovmpodv2  6212  fvmpopr2d  6215  elovmporab  6279  elovmporab1w  6280  ofvalg  6302  ofrval  6303  off  6305  ofres  6307  suppssof1  6310  ofco  6311  caofref  6317  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  caofrss  6324  caoftrn  6325  uchoice  6361  suppofss1dcl  6494  suppofss2dcl  6495  rdgivallem  6642  iserd  6823  ixpsnf1o  7008  modom  7098  1domsn  7105  mapxpen  7138  infnninf  7454  ctssexmid  7480  nninfdcinf  7501  nninfwlporlemd  7502  nninfwlporlem  7503  nninfwlpoimlemginf  7506  nninfinfwlpo  7510  ofnegsub  9282  infrenegsupex  9973  fz0to4untppr  10509  fzo0to3tp  10615  modqsubmod  10797  0tonninf  10855  iseqovex  10873  seqvalcd  10876  seq3f1olemqsumkj  10926  seq3id  10940  seq3id2  10941  ccatws1ls  11388  pfxsuffeqwrdeq  11448  wrdind  11472  wrd2ind  11473  ccats1pfxeqbi  11492  s3eq2  11527  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrex  11770  infxrnegsupex  12007  climcl  12026  clim2  12027  climuni  12037  climeq  12043  2clim  12045  climshftlemg  12046  climabs0  12051  climcn1  12052  climcn2  12053  climge0  12069  climsqz  12079  climsqz2  12080  climcau  12091  climrecvg1n  12092  climcaucn  12095  serf0  12096  fzf1o  12120  isumz  12134  fisumss  12137  fsumsplitsn  12155  fsumsplitsnun  12164  isumclim3  12168  isummulc2  12171  fsum2dlemstep  12179  fsumconst  12199  fsumabs  12210  fsumparts  12215  iserabs  12220  fsumiun  12222  isumshft  12235  cvgratnnlemseq  12271  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  prod1dc  12331  fprodssdc  12335  fprodunsn  12349  fprodcl2lem  12350  fprodconst  12365  fprod2dlemstep  12367  fprodsplitsn  12378  eftlcl  12433  reeftlcl  12434  eftlub  12435  efsep  12436  effsumlt  12437  eirraplem  12522  2tp1odd  12629  bezoutlemstep  12752  nninfctlemfo  12795  alginv  12803  algfx  12808  cncongr1  12859  qnumdencoprm  12949  qeqnumdivden  12950  ballotfilemgun  13246  ballotfilemfg  13247  ballotfilemfrc  13248  ctiunctal  13310  unct  13311  nninfdclemcl  13317  nninfdclemf  13318  nninfdclemp1  13319  nninfdc  13322  ressbasid  13401  ressressg  13406  imasex  13603  imasbas  13605  imasplusg  13606  imasmulr  13607  qusin  13624  gzsumvalx  13686  gzsumfzval  13688  gzsum0  13690  gzsumval2  13691  issgrp  13695  sgrp1  13703  issgrpd  13704  ismndd  13727  mndprop  13731  ress0g  13733  imasmnd2  13736  insubm  13769  resmhm  13771  resmhm2  13772  resmhm2b  13773  grpprop  13800  grpsubfvalg  13827  grpressid  13843  grpsubpropdg  13886  imasgrp2  13890  imasgrp  13891  imasgrpf1  13892  mulgfvalg  13901  mulgnngzsum  13907  mulgpropdg  13944  submmulg  13946  subginv  13961  subgcl  13964  subgsub  13966  releqgg  14000  eqgex  14001  eqgfval  14002  qusgrp  14012  resghm  14040  ablprop  14077  cmnsubm  14089  subcmnd  14114  ablressid  14116  gzsumconst  14120  gzsumconstf  14121  gzsummhm2  14123  gzsumsplit0  14125  gzsumshift  14126  gsumvalfi  14129  gzsumgsum  14132  gsumsncmn  14133  gsumzfi  14135  gsummhm2fi  14142  prdsex  14149  prdsbaslemss  14151  prdssca  14152  prdsbas  14153  prdsplusg  14154  prdsmulr  14155  prdssgrpd  14168  prdsmndd  14171  prdsgrpd  14174  isrng  14208  isrngd  14227  rngressid  14228  imasrng  14230  issrg  14243  srgidmlem  14256  isring  14278  ringass  14294  ringidmlem  14300  ringabl  14310  ringprop  14318  isringd  14319  ring1  14337  ringressid  14341  imasring  14342  opprrng  14355  opprring  14357  opprringbg  14358  opprsubgg  14363  mulgass3  14364  dvdsrcld  14377  dvdsrex  14378  dvdsrcl2  14379  dvdsrid  14380  dvdsrtr  14381  dvdsrneg  14383  dvdsr01  14384  1unit  14387  unitcld  14388  opprunitd  14390  crngunit  14391  unitmulcl  14393  unitgrpbasd  14395  unitgrp  14396  unitabl  14397  unitgrpid  14398  unitsubm  14399  unitlinv  14406  unitrinv  14407  unitnegcl  14410  dvrfvald  14413  dvrvald  14414  dvrcl  14415  unitdvcl  14416  dvrid  14417  dvr1  14418  dvrdir  14423  rdivmuldivd  14424  dvdsrpropdg  14427  unitpropdg  14428  invrpropdg  14429  rhmf1o  14448  rhmdvdsr  14455  elrhmunit  14457  rhmunitinv  14458  opprlring  14477  issubrng2  14491  subrngpropd  14497  subrgcrng  14506  subrgdvds  14516  subrguss  14517  subrginv  14518  subrgdv  14519  subrgunit  14520  subrgugrp  14521  issubrg2  14522  subrgpropd  14534  aprunit  14565  aprirr  14568  aprsym  14569  aprcotr  14570  aprap  14571  aprnzr  14572  aprlring  14573  aprprop  14574  opprdrng  14593  islmodd  14602  lmodabl  14643  lss1  14671  lsssn0  14679  islss3  14688  lss1d  14692  lssintclm  14693  lsslsp  14738  sralmod  14759  sralmod0g  14760  rlmfn  14762  rlmvalg  14763  rlm0g  14766  rlmvnegg  14774  lidlssbas  14786  islidlm  14788  rnglidlmsgrp  14806  rnglidlrng  14807  qus2idrng  14834  crngridl  14839  quscrng  14842  cnfldui  14896  dvdsrzring  14910  zrhpropd  14933  znzrh  14950  znbas  14951  zncrng  14952  znzrhfo  14955  znf1o  14958  znunit  14966  psrval  14973  psrbaglesuppg  14980  psrbagcon  14985  psrbagconf1o  14987  psrbasg  14988  psrplusgg  14992  mplsubgfilemcl  15013  mplplusgg  15017  epttop  15114  lmss  15270  txlm  15303  lmcn2  15304  cnmpt2c  15314  txswaphmeolem  15344  blfvalps  15409  bdxmet  15525  mpomulcn  15590  fsumcncntop  15591  cncfmptc  15620  cncfmpt1f  15622  cdivcncfap  15628  negfcncf  15630  divcncfap  15638  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dviaddf  15729  dvexp  15735  dvmptaddx  15743  dvmptmulx  15744  dvmptfsum  15749  dvef  15751  elply2  15759  elplyr  15764  plyaddlem1  15771  plycolemc  15782  sincn  15793  coscn  15794  logfac  15918  lgsdir2lem5  16065  gausslemma2dlem1  16094  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquad2lem2  16115  2lgslem1b  16122  2lgslem3b1  16131  2lgslem3c1  16132  2lgsoddprmlem4  16145  2sqlem8  16156  usgredg4  16370  ushgredgedg  16381  ushgredgedgloop  16383  usgrstrrepeen  16386  uspgr1edc  16395  wlk1walkdom  16514  uspgr2wlkeq  16520  uspgr2wlkeqi  16522  clwwlknonmpo  16583  iseupth  16602  eupth2lem2dc  16614  konigsberglem2  16644  konigsberglem3  16645  nninfsellemeqinf  16964  nninffeq  16968  nnnninfex  16970  exmidsbthrlem  16972  cvgcmp2nlemabs  16986