Theorem eqidd 2210

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

Syntax hints:   → wi 4   = wceq 1375

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 1475  ax-ext 2191

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

This theorem is referenced by:  cbvraldva  2754  cbvrexdva  2755  rspcedeq1vd  2896  rspcedeq2vd  2897  nelrdva  2990  opeq2  3837  mpteq1  4147  tfisi  4656  feq23d  5445  f10d  5583  fvmptdv2  5697  elrnrexdm  5747  fmptco  5774  cofmpt  5777  ftpg  5796  fliftfun  5893  fliftval  5897  cbvmpo  6054  fconstmpo  6070  eqfnov2  6083  ovmpod  6103  ovmpodv2  6109  fvmpopr2d  6112  elovmporab  6176  elovmporab1w  6177  ofvalg  6198  ofrval  6199  off  6201  ofres  6203  suppssof1  6206  ofco  6207  caofref  6213  caofid0l  6215  caofid0r  6216  caofid1  6217  caofid2  6218  caofrss  6220  caoftrn  6221  uchoice  6253  rdgivallem  6497  iserd  6676  ixpsnf1o  6853  1domsn  6946  mapxpen  6977  infnninf  7259  ctssexmid  7285  nninfdcinf  7306  nninfwlporlemd  7307  nninfwlporlem  7308  nninfwlpoimlemginf  7311  nninfinfwlpo  7315  ofnegsub  9077  infrenegsupex  9757  fz0to4untppr  10288  fzo0to3tp  10392  modqsubmod  10571  0tonninf  10629  iseqovex  10647  seqvalcd  10650  seq3f1olemqsumkj  10700  seq3id  10714  seq3id2  10715  ccatws1ls  11139  pfxsuffeqwrdeq  11196  wrdind  11220  wrd2ind  11221  ccats1pfxeqbi  11240  s3eq2  11275  resqrexlemp1rp  11483  resqrexlemfp1  11486  resqrex  11503  infxrnegsupex  11740  climcl  11759  clim2  11760  climuni  11770  climeq  11776  2clim  11778  climshftlemg  11779  climabs0  11784  climcn1  11785  climcn2  11786  climge0  11802  climsqz  11812  climsqz2  11813  climcau  11824  climrecvg1n  11825  climcaucn  11828  serf0  11829  isumz  11866  fisumss  11869  fsumsplitsn  11887  fsumsplitsnun  11896  isumclim3  11900  isummulc2  11903  fsum2dlemstep  11911  fsumconst  11931  fsumabs  11942  fsumparts  11947  iserabs  11952  fsumiun  11954  isumshft  11967  cvgratnnlemseq  12003  mertenslemub  12011  mertenslemi1  12012  mertenslem2  12013  prod1dc  12063  fprodssdc  12067  fprodunsn  12081  fprodcl2lem  12082  fprodconst  12097  fprod2dlemstep  12099  fprodsplitsn  12110  eftlcl  12165  reeftlcl  12166  eftlub  12167  efsep  12168  effsumlt  12169  eirraplem  12254  2tp1odd  12361  bezoutlemstep  12484  nninfctlemfo  12527  alginv  12535  algfx  12540  cncongr1  12591  qnumdencoprm  12681  qeqnumdivden  12682  ctiunctal  12978  unct  12979  nninfdclemcl  12985  nninfdclemf  12986  nninfdclemp1  12987  nninfdc  12990  ressbasid  13069  ressressg  13074  prdsex  13268  prdsbaslemss  13273  prdssca  13274  prdsbas  13275  prdsplusg  13276  prdsmulr  13277  imasex  13304  imasbas  13306  imasplusg  13307  imasmulr  13308  qusin  13325  igsumvalx  13388  gsumfzval  13390  gsumpropd  13391  gsumpropd2  13392  gsum0g  13395  gsumval2  13396  issgrp  13402  sgrp1  13410  issgrpd  13411  prdssgrpd  13414  ismndd  13436  mndprop  13440  ress0g  13442  prdsmndd  13447  imasmnd2  13451  insubm  13484  resmhm  13486  resmhm2  13487  resmhm2b  13488  gsumfzz  13494  grpprop  13517  grpsubfvalg  13544  grpressid  13560  grpsubpropdg  13603  prdsgrpd  13608  imasgrp2  13613  imasgrp  13614  imasgrpf1  13615  mulgfvalg  13624  mulgnngsum  13630  mulgpropdg  13667  submmulg  13669  subginv  13684  subgcl  13687  subgsub  13689  releqgg  13723  eqgex  13724  eqgfval  13725  qusgrp  13735  resghm  13763  ablprop  13800  subcmnd  13836  ablressid  13838  gsumfzmptfidmadd  13842  gsumfzconst  13844  gsumfzconstf  13845  gsumfzmhm2  13847  isrng  13863  isrngd  13882  rngressid  13883  imasrng  13885  issrg  13894  srgidmlem  13907  isring  13929  ringass  13945  ringidmlem  13951  ringabl  13961  ringprop  13969  isringd  13970  ring1  13988  ringressid  13992  imasring  13993  opprrng  14006  opprring  14008  opprringbg  14009  opprsubgg  14013  mulgass3  14014  dvdsrcld  14026  dvdsrex  14027  dvdsrcl2  14028  dvdsrid  14029  dvdsrtr  14030  dvdsrneg  14032  dvdsr01  14033  1unit  14036  unitcld  14037  opprunitd  14039  crngunit  14040  unitmulcl  14042  unitgrpbasd  14044  unitgrp  14045  unitabl  14046  unitgrpid  14047  unitsubm  14048  unitlinv  14055  unitrinv  14056  unitnegcl  14059  dvrfvald  14062  dvrvald  14063  dvrcl  14064  unitdvcl  14065  dvrid  14066  dvr1  14067  dvrdir  14072  rdivmuldivd  14073  dvdsrpropdg  14076  unitpropdg  14077  invrpropdg  14078  rhmf1o  14097  rhmdvdsr  14104  elrhmunit  14106  rhmunitinv  14107  issubrng2  14139  subrngpropd  14145  subrgcrng  14154  subrgdvds  14164  subrguss  14165  subrginv  14166  subrgdv  14167  subrgunit  14168  subrgugrp  14169  issubrg2  14170  subrgpropd  14182  aprirr  14212  aprsym  14213  aprcotr  14214  aprap  14215  islmodd  14222  lmodabl  14263  lss1  14291  lsssn0  14299  islss3  14308  lss1d  14312  lssintclm  14313  lsslsp  14358  sralmod  14379  sralmod0g  14380  rlmfn  14382  rlmvalg  14383  rlm0g  14386  rlmvnegg  14394  lidlssbas  14406  islidlm  14408  rnglidlmsgrp  14426  rnglidlrng  14427  qus2idrng  14454  crngridl  14459  quscrng  14462  cnfldui  14518  dvdsrzring  14532  zrhpropd  14555  znzrh  14572  znbas  14573  zncrng  14574  znzrhfo  14577  znf1o  14580  znunit  14588  psrval  14595  psrbaglesuppg  14601  psrbasg  14603  psrplusgg  14607  mplsubgfilemcl  14628  mplplusgg  14632  epttop  14729  lmss  14885  txlm  14918  lmcn2  14919  cnmpt2c  14929  txswaphmeolem  14959  blfvalps  15024  bdxmet  15140  mpomulcn  15205  fsumcncntop  15206  cncfmptc  15235  cncfmpt1f  15237  cdivcncfap  15243  negfcncf  15245  divcncfap  15253  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvcnp2cntop  15338  dvaddxxbr  15340  dvmulxxbr  15341  dviaddf  15344  dvexp  15350  dvmptaddx  15358  dvmptmulx  15359  dvmptfsum  15364  dvef  15366  elply2  15374  elplyr  15379  plyaddlem1  15386  plycolemc  15397  sincn  15408  coscn  15409  lgsdir2lem5  15676  gausslemma2dlem1  15705  lgseisenlem2  15715  lgseisenlem3  15716  lgseisenlem4  15717  lgsquad2lem2  15726  2lgslem1b  15733  2lgslem3b1  15742  2lgslem3c1  15743  2lgsoddprmlem4  15756  2sqlem8  15767  usgredg4  15978  ushgredgedg  15989  ushgredgedgloop  15991  usgrstrrepeen  15994  nninfsellemeqinf  16293  nninffeq  16297  nnnninfex  16299  exmidsbthrlem  16301  cvgcmp2nlemabs  16311