Theorem eqidd 2232

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 2231	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 9	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1397

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 1497  ax-ext 2213

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

This theorem is referenced by:  cbvraldva  2776  cbvrexdva  2777  rspcedeq1vd  2919  rspcedeq2vd  2920  nelrdva  3013  opeq2  3863  mpteq1  4173  tfisi  4685  feq23d  5478  f10d  5619  fvmptdv2  5736  elrnrexdm  5786  fmptco  5813  cofmpt  5816  ftpg  5838  fliftfun  5937  fliftval  5941  cbvmpo  6100  fconstmpo  6116  eqfnov2  6129  ovmpod  6149  ovmpodv2  6155  fvmpopr2d  6158  elovmporab  6222  elovmporab1w  6223  ofvalg  6245  ofrval  6246  off  6248  ofres  6250  suppssof1  6253  ofco  6254  caofref  6260  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  caofrss  6267  caoftrn  6268  uchoice  6300  rdgivallem  6547  iserd  6728  ixpsnf1o  6905  modom  6994  1domsn  7001  mapxpen  7034  infnninf  7323  ctssexmid  7349  nninfdcinf  7370  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemginf  7375  nninfinfwlpo  7379  ofnegsub  9142  infrenegsupex  9828  fz0to4untppr  10359  fzo0to3tp  10465  modqsubmod  10645  0tonninf  10703  iseqovex  10721  seqvalcd  10724  seq3f1olemqsumkj  10774  seq3id  10788  seq3id2  10789  ccatws1ls  11220  pfxsuffeqwrdeq  11280  wrdind  11304  wrd2ind  11305  ccats1pfxeqbi  11324  s3eq2  11359  resqrexlemp1rp  11568  resqrexlemfp1  11571  resqrex  11588  infxrnegsupex  11825  climcl  11844  clim2  11845  climuni  11855  climeq  11861  2clim  11863  climshftlemg  11864  climabs0  11869  climcn1  11870  climcn2  11871  climge0  11887  climsqz  11897  climsqz2  11898  climcau  11909  climrecvg1n  11910  climcaucn  11913  serf0  11914  fzf1o  11938  isumz  11952  fisumss  11955  fsumsplitsn  11973  fsumsplitsnun  11982  isumclim3  11986  isummulc2  11989  fsum2dlemstep  11997  fsumconst  12017  fsumabs  12028  fsumparts  12033  iserabs  12038  fsumiun  12040  isumshft  12053  cvgratnnlemseq  12089  mertenslemub  12097  mertenslemi1  12098  mertenslem2  12099  prod1dc  12149  fprodssdc  12153  fprodunsn  12167  fprodcl2lem  12168  fprodconst  12183  fprod2dlemstep  12185  fprodsplitsn  12196  eftlcl  12251  reeftlcl  12252  eftlub  12253  efsep  12254  effsumlt  12255  eirraplem  12340  2tp1odd  12447  bezoutlemstep  12570  nninfctlemfo  12613  alginv  12621  algfx  12626  cncongr1  12677  qnumdencoprm  12767  qeqnumdivden  12768  ctiunctal  13064  unct  13065  nninfdclemcl  13071  nninfdclemf  13072  nninfdclemp1  13073  nninfdc  13076  ressbasid  13155  ressressg  13160  prdsex  13354  prdsbaslemss  13359  prdssca  13360  prdsbas  13361  prdsplusg  13362  prdsmulr  13363  imasex  13390  imasbas  13392  imasplusg  13393  imasmulr  13394  qusin  13411  igsumvalx  13474  gsumfzval  13476  gsumpropd  13477  gsumpropd2  13478  gsum0g  13481  gsumval2  13482  issgrp  13488  sgrp1  13496  issgrpd  13497  prdssgrpd  13500  ismndd  13522  mndprop  13526  ress0g  13528  prdsmndd  13533  imasmnd2  13537  insubm  13570  resmhm  13572  resmhm2  13573  resmhm2b  13574  gsumfzz  13580  grpprop  13603  grpsubfvalg  13630  grpressid  13646  grpsubpropdg  13689  prdsgrpd  13694  imasgrp2  13699  imasgrp  13700  imasgrpf1  13701  mulgfvalg  13710  mulgnngsum  13716  mulgpropdg  13753  submmulg  13755  subginv  13770  subgcl  13773  subgsub  13775  releqgg  13809  eqgex  13810  eqgfval  13811  qusgrp  13821  resghm  13849  ablprop  13886  subcmnd  13922  ablressid  13924  gsumfzmptfidmadd  13928  gsumfzconst  13930  gsumfzconstf  13931  gsumfzmhm2  13933  gsumsplit0  13935  isrng  13950  isrngd  13969  rngressid  13970  imasrng  13972  issrg  13981  srgidmlem  13994  isring  14016  ringass  14032  ringidmlem  14038  ringabl  14048  ringprop  14056  isringd  14057  ring1  14075  ringressid  14079  imasring  14080  opprrng  14093  opprring  14095  opprringbg  14096  opprsubgg  14100  mulgass3  14101  dvdsrcld  14114  dvdsrex  14115  dvdsrcl2  14116  dvdsrid  14117  dvdsrtr  14118  dvdsrneg  14120  dvdsr01  14121  1unit  14124  unitcld  14125  opprunitd  14127  crngunit  14128  unitmulcl  14130  unitgrpbasd  14132  unitgrp  14133  unitabl  14134  unitgrpid  14135  unitsubm  14136  unitlinv  14143  unitrinv  14144  unitnegcl  14147  dvrfvald  14150  dvrvald  14151  dvrcl  14152  unitdvcl  14153  dvrid  14154  dvr1  14155  dvrdir  14160  rdivmuldivd  14161  dvdsrpropdg  14164  unitpropdg  14165  invrpropdg  14166  rhmf1o  14185  rhmdvdsr  14192  elrhmunit  14194  rhmunitinv  14195  issubrng2  14227  subrngpropd  14233  subrgcrng  14242  subrgdvds  14252  subrguss  14253  subrginv  14254  subrgdv  14255  subrgunit  14256  subrgugrp  14257  issubrg2  14258  subrgpropd  14270  aprirr  14300  aprsym  14301  aprcotr  14302  aprap  14303  islmodd  14310  lmodabl  14351  lss1  14379  lsssn0  14387  islss3  14396  lss1d  14400  lssintclm  14401  lsslsp  14446  sralmod  14467  sralmod0g  14468  rlmfn  14470  rlmvalg  14471  rlm0g  14474  rlmvnegg  14482  lidlssbas  14494  islidlm  14496  rnglidlmsgrp  14514  rnglidlrng  14515  qus2idrng  14542  crngridl  14547  quscrng  14550  cnfldui  14606  dvdsrzring  14620  zrhpropd  14643  znzrh  14660  znbas  14661  zncrng  14662  znzrhfo  14665  znf1o  14668  znunit  14676  psrval  14683  psrbaglesuppg  14689  psrbasg  14691  psrplusgg  14695  mplsubgfilemcl  14716  mplplusgg  14720  epttop  14817  lmss  14973  txlm  15006  lmcn2  15007  cnmpt2c  15017  txswaphmeolem  15047  blfvalps  15112  bdxmet  15228  mpomulcn  15293  fsumcncntop  15294  cncfmptc  15323  cncfmpt1f  15325  cdivcncfap  15331  negfcncf  15333  divcncfap  15341  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dviaddf  15432  dvexp  15438  dvmptaddx  15446  dvmptmulx  15447  dvmptfsum  15452  dvef  15454  elply2  15462  elplyr  15467  plyaddlem1  15474  plycolemc  15485  sincn  15496  coscn  15497  lgsdir2lem5  15764  gausslemma2dlem1  15793  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  lgsquad2lem2  15814  2lgslem1b  15821  2lgslem3b1  15830  2lgslem3c1  15831  2lgsoddprmlem4  15844  2sqlem8  15855  usgredg4  16069  ushgredgedg  16080  ushgredgedgloop  16082  usgrstrrepeen  16085  uspgr1edc  16094  wlk1walkdom  16213  uspgr2wlkeq  16219  uspgr2wlkeqi  16221  clwwlknonmpo  16282  iseupth  16301  eupth2lem2dc  16313  nninfsellemeqinf  16639  nninffeq  16643  nnnninfex  16645  exmidsbthrlem  16647  cvgcmp2nlemabs  16657  gfsumval  16701  gsumgfsumlem  16704  gsumgfsum  16705  gfsumsn  16706