Theorem eqidd 2206

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 2205	. 2 |- A = A
2	1	a1i 9	1 |- ( ph -> A = A )

Syntax hints:   -> wi 4   = wceq 1373

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 1472  ax-ext 2187

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

This theorem is referenced by:  cbvraldva  2747  cbvrexdva  2748  rspcedeq1vd  2886  rspcedeq2vd  2887  nelrdva  2980  opeq2  3820  mpteq1  4128  tfisi  4635  feq23d  5421  fvmptdv2  5669  elrnrexdm  5719  fmptco  5746  cofmpt  5749  ftpg  5768  fliftfun  5865  fliftval  5869  cbvmpo  6024  fconstmpo  6040  eqfnov2  6053  ovmpod  6073  ovmpodv2  6079  fvmpopr2d  6082  elovmporab  6146  elovmporab1w  6147  ofvalg  6168  ofrval  6169  off  6171  ofres  6173  suppssof1  6176  ofco  6177  caofref  6183  caofid0l  6185  caofid0r  6186  caofid1  6187  caofid2  6188  caofrss  6190  caoftrn  6191  uchoice  6223  rdgivallem  6467  iserd  6646  ixpsnf1o  6823  1domsn  6914  mapxpen  6945  infnninf  7226  ctssexmid  7252  nninfdcinf  7273  nninfwlporlemd  7274  nninfwlporlem  7275  nninfwlpoimlemginf  7278  nninfinfwlpo  7282  ofnegsub  9035  infrenegsupex  9715  fz0to4untppr  10246  fzo0to3tp  10348  modqsubmod  10527  0tonninf  10585  iseqovex  10603  seqvalcd  10606  seq3f1olemqsumkj  10656  seq3id  10670  seq3id2  10671  ccatws1ls  11094  resqrexlemp1rp  11317  resqrexlemfp1  11320  resqrex  11337  infxrnegsupex  11574  climcl  11593  clim2  11594  climuni  11604  climeq  11610  2clim  11612  climshftlemg  11613  climabs0  11618  climcn1  11619  climcn2  11620  climge0  11636  climsqz  11646  climsqz2  11647  climcau  11658  climrecvg1n  11659  climcaucn  11662  serf0  11663  isumz  11700  fisumss  11703  fsumsplitsn  11721  fsumsplitsnun  11730  isumclim3  11734  isummulc2  11737  fsum2dlemstep  11745  fsumconst  11765  fsumabs  11776  fsumparts  11781  iserabs  11786  fsumiun  11788  isumshft  11801  cvgratnnlemseq  11837  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  prod1dc  11897  fprodssdc  11901  fprodunsn  11915  fprodcl2lem  11916  fprodconst  11931  fprod2dlemstep  11933  fprodsplitsn  11944  eftlcl  11999  reeftlcl  12000  eftlub  12001  efsep  12002  effsumlt  12003  eirraplem  12088  2tp1odd  12195  bezoutlemstep  12318  nninfctlemfo  12361  alginv  12369  algfx  12374  cncongr1  12425  qnumdencoprm  12515  qeqnumdivden  12516  ctiunctal  12812  unct  12813  nninfdclemcl  12819  nninfdclemf  12820  nninfdclemp1  12821  nninfdc  12824  ressbasid  12902  ressressg  12907  prdsex  13101  prdsbaslemss  13106  prdssca  13107  prdsbas  13108  prdsplusg  13109  prdsmulr  13110  imasex  13137  imasbas  13139  imasplusg  13140  imasmulr  13141  qusin  13158  igsumvalx  13221  gsumfzval  13223  gsumpropd  13224  gsumpropd2  13225  gsum0g  13228  gsumval2  13229  issgrp  13235  sgrp1  13243  issgrpd  13244  prdssgrpd  13247  ismndd  13269  mndprop  13273  ress0g  13275  prdsmndd  13280  imasmnd2  13284  insubm  13317  resmhm  13319  resmhm2  13320  resmhm2b  13321  gsumfzz  13327  grpprop  13350  grpsubfvalg  13377  grpressid  13393  grpsubpropdg  13436  prdsgrpd  13441  imasgrp2  13446  imasgrp  13447  imasgrpf1  13448  mulgfvalg  13457  mulgnngsum  13463  mulgpropdg  13500  submmulg  13502  subginv  13517  subgcl  13520  subgsub  13522  releqgg  13556  eqgex  13557  eqgfval  13558  qusgrp  13568  resghm  13596  ablprop  13633  subcmnd  13669  ablressid  13671  gsumfzmptfidmadd  13675  gsumfzconst  13677  gsumfzconstf  13678  gsumfzmhm2  13680  isrng  13696  isrngd  13715  rngressid  13716  imasrng  13718  issrg  13727  srgidmlem  13740  isring  13762  ringass  13778  ringidmlem  13784  ringabl  13794  ringprop  13802  isringd  13803  ring1  13821  ringressid  13825  imasring  13826  opprrng  13839  opprring  13841  opprringbg  13842  opprsubgg  13846  mulgass3  13847  dvdsrcld  13859  dvdsrex  13860  dvdsrcl2  13861  dvdsrid  13862  dvdsrtr  13863  dvdsrneg  13865  dvdsr01  13866  1unit  13869  unitcld  13870  opprunitd  13872  crngunit  13873  unitmulcl  13875  unitgrpbasd  13877  unitgrp  13878  unitabl  13879  unitgrpid  13880  unitsubm  13881  unitlinv  13888  unitrinv  13889  unitnegcl  13892  dvrfvald  13895  dvrvald  13896  dvrcl  13897  unitdvcl  13898  dvrid  13899  dvr1  13900  dvrdir  13905  rdivmuldivd  13906  dvdsrpropdg  13909  unitpropdg  13910  invrpropdg  13911  rhmf1o  13930  rhmdvdsr  13937  elrhmunit  13939  rhmunitinv  13940  issubrng2  13972  subrngpropd  13978  subrgcrng  13987  subrgdvds  13997  subrguss  13998  subrginv  13999  subrgdv  14000  subrgunit  14001  subrgugrp  14002  issubrg2  14003  subrgpropd  14015  aprirr  14045  aprsym  14046  aprcotr  14047  aprap  14048  islmodd  14055  lmodabl  14096  lss1  14124  lsssn0  14132  islss3  14141  lss1d  14145  lssintclm  14146  lsslsp  14191  sralmod  14212  sralmod0g  14213  rlmfn  14215  rlmvalg  14216  rlm0g  14219  rlmvnegg  14227  lidlssbas  14239  islidlm  14241  rnglidlmsgrp  14259  rnglidlrng  14260  qus2idrng  14287  crngridl  14292  quscrng  14295  cnfldui  14351  dvdsrzring  14365  zrhpropd  14388  znzrh  14405  znbas  14406  zncrng  14407  znzrhfo  14410  znf1o  14413  znunit  14421  psrval  14428  psrbaglesuppg  14434  psrbasg  14436  psrplusgg  14440  mplsubgfilemcl  14461  mplplusgg  14465  epttop  14562  lmss  14718  txlm  14751  lmcn2  14752  cnmpt2c  14762  txswaphmeolem  14792  blfvalps  14857  bdxmet  14973  mpomulcn  15038  fsumcncntop  15039  cncfmptc  15068  cncfmpt1f  15070  cdivcncfap  15076  negfcncf  15078  divcncfap  15086  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dviaddf  15177  dvexp  15183  dvmptaddx  15191  dvmptmulx  15192  dvmptfsum  15197  dvef  15199  elply2  15207  elplyr  15212  plyaddlem1  15219  plycolemc  15230  sincn  15241  coscn  15242  lgsdir2lem5  15509  gausslemma2dlem1  15538  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquad2lem2  15559  2lgslem1b  15566  2lgslem3b1  15575  2lgslem3c1  15576  2lgsoddprmlem4  15589  2sqlem8  15600  nninfsellemeqinf  15953  nninffeq  15957  nnnninfex  15959  exmidsbthrlem  15961  cvgcmp2nlemabs  15971