Theorem eqidd 2197

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

Syntax hints:   → wi 4   = wceq 1364

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 1463  ax-ext 2178

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

This theorem is referenced by:  cbvraldva  2738  cbvrexdva  2739  rspcedeq1vd  2877  rspcedeq2vd  2878  nelrdva  2971  opeq2  3810  mpteq1  4118  tfisi  4624  feq23d  5406  fvmptdv2  5654  elrnrexdm  5704  fmptco  5731  cofmpt  5734  ftpg  5749  fliftfun  5846  fliftval  5850  cbvmpo  6005  fconstmpo  6021  eqfnov2  6034  ovmpod  6054  ovmpodv2  6060  fvmpopr2d  6063  elovmporab  6127  elovmporab1w  6128  ofvalg  6149  ofrval  6150  off  6152  ofres  6154  suppssof1  6157  ofco  6158  caofref  6164  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  caofrss  6171  caoftrn  6172  uchoice  6204  rdgivallem  6448  iserd  6627  ixpsnf1o  6804  1domsn  6887  mapxpen  6918  infnninf  7199  ctssexmid  7225  nninfdcinf  7246  nninfwlporlemd  7247  nninfwlporlem  7248  nninfwlpoimlemginf  7251  ofnegsub  9006  infrenegsupex  9685  fz0to4untppr  10216  fzo0to3tp  10312  modqsubmod  10491  0tonninf  10549  iseqovex  10567  seqvalcd  10570  seq3f1olemqsumkj  10620  seq3id  10634  seq3id2  10635  resqrexlemp1rp  11188  resqrexlemfp1  11191  resqrex  11208  infxrnegsupex  11445  climcl  11464  clim2  11465  climuni  11475  climeq  11481  2clim  11483  climshftlemg  11484  climabs0  11489  climcn1  11490  climcn2  11491  climge0  11507  climsqz  11517  climsqz2  11518  climcau  11529  climrecvg1n  11530  climcaucn  11533  serf0  11534  isumz  11571  fisumss  11574  fsumsplitsn  11592  fsumsplitsnun  11601  isumclim3  11605  isummulc2  11608  fsum2dlemstep  11616  fsumconst  11636  fsumabs  11647  fsumparts  11652  iserabs  11657  fsumiun  11659  isumshft  11672  cvgratnnlemseq  11708  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  prod1dc  11768  fprodssdc  11772  fprodunsn  11786  fprodcl2lem  11787  fprodconst  11802  fprod2dlemstep  11804  fprodsplitsn  11815  eftlcl  11870  reeftlcl  11871  eftlub  11872  efsep  11873  effsumlt  11874  eirraplem  11959  2tp1odd  12066  bezoutlemstep  12189  nninfctlemfo  12232  alginv  12240  algfx  12245  cncongr1  12296  qnumdencoprm  12386  qeqnumdivden  12387  ctiunctal  12683  unct  12684  nninfdclemcl  12690  nninfdclemf  12691  nninfdclemp1  12692  nninfdc  12695  ressbasid  12773  ressressg  12778  prdsex  12971  prdsbaslemss  12976  prdssca  12977  prdsbas  12978  prdsplusg  12979  prdsmulr  12980  imasex  13007  imasbas  13009  imasplusg  13010  imasmulr  13011  qusin  13028  igsumvalx  13091  gsumfzval  13093  gsumpropd  13094  gsumpropd2  13095  gsum0g  13098  gsumval2  13099  issgrp  13105  sgrp1  13113  issgrpd  13114  prdssgrpd  13117  ismndd  13139  mndprop  13143  ress0g  13145  prdsmndd  13150  imasmnd2  13154  insubm  13187  resmhm  13189  resmhm2  13190  resmhm2b  13191  gsumfzz  13197  grpprop  13220  grpsubfvalg  13247  grpressid  13263  grpsubpropdg  13306  prdsgrpd  13311  imasgrp2  13316  imasgrp  13317  imasgrpf1  13318  mulgfvalg  13327  mulgnngsum  13333  mulgpropdg  13370  submmulg  13372  subginv  13387  subgcl  13390  subgsub  13392  releqgg  13426  eqgex  13427  eqgfval  13428  qusgrp  13438  resghm  13466  ablprop  13503  subcmnd  13539  ablressid  13541  gsumfzmptfidmadd  13545  gsumfzconst  13547  gsumfzconstf  13548  gsumfzmhm2  13550  isrng  13566  isrngd  13585  rngressid  13586  imasrng  13588  issrg  13597  srgidmlem  13610  isring  13632  ringass  13648  ringidmlem  13654  ringabl  13664  ringprop  13672  isringd  13673  ring1  13691  ringressid  13695  imasring  13696  opprrng  13709  opprring  13711  opprringbg  13712  opprsubgg  13716  mulgass3  13717  dvdsrcld  13729  dvdsrex  13730  dvdsrcl2  13731  dvdsrid  13732  dvdsrtr  13733  dvdsrneg  13735  dvdsr01  13736  1unit  13739  unitcld  13740  opprunitd  13742  crngunit  13743  unitmulcl  13745  unitgrpbasd  13747  unitgrp  13748  unitabl  13749  unitgrpid  13750  unitsubm  13751  unitlinv  13758  unitrinv  13759  unitnegcl  13762  dvrfvald  13765  dvrvald  13766  dvrcl  13767  unitdvcl  13768  dvrid  13769  dvr1  13770  dvrdir  13775  rdivmuldivd  13776  dvdsrpropdg  13779  unitpropdg  13780  invrpropdg  13781  rhmf1o  13800  rhmdvdsr  13807  elrhmunit  13809  rhmunitinv  13810  issubrng2  13842  subrngpropd  13848  subrgcrng  13857  subrgdvds  13867  subrguss  13868  subrginv  13869  subrgdv  13870  subrgunit  13871  subrgugrp  13872  issubrg2  13873  subrgpropd  13885  aprirr  13915  aprsym  13916  aprcotr  13917  aprap  13918  islmodd  13925  lmodabl  13966  lss1  13994  lsssn0  14002  islss3  14011  lss1d  14015  lssintclm  14016  lsslsp  14061  sralmod  14082  sralmod0g  14083  rlmfn  14085  rlmvalg  14086  rlm0g  14089  rlmvnegg  14097  lidlssbas  14109  islidlm  14111  rnglidlmsgrp  14129  rnglidlrng  14130  qus2idrng  14157  crngridl  14162  quscrng  14165  cnfldui  14221  dvdsrzring  14235  zrhpropd  14258  znzrh  14275  znbas  14276  zncrng  14277  znzrhfo  14280  znf1o  14283  znunit  14291  psrval  14296  psrbaglesuppg  14302  psrbasg  14303  psrplusgg  14306  epttop  14410  lmss  14566  txlm  14599  lmcn2  14600  cnmpt2c  14610  txswaphmeolem  14640  blfvalps  14705  bdxmet  14821  mpomulcn  14886  fsumcncntop  14887  cncfmptc  14916  cncfmpt1f  14918  cdivcncfap  14924  negfcncf  14926  divcncfap  14934  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dviaddf  15025  dvexp  15031  dvmptaddx  15039  dvmptmulx  15040  dvmptfsum  15045  dvef  15047  elply2  15055  elplyr  15060  plyaddlem1  15067  plycolemc  15078  sincn  15089  coscn  15090  lgsdir2lem5  15357  gausslemma2dlem1  15386  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquad2lem2  15407  2lgslem1b  15414  2lgslem3b1  15423  2lgslem3c1  15424  2lgsoddprmlem4  15437  2sqlem8  15448  nninfsellemeqinf  15747  nninffeq  15751  exmidsbthrlem  15753  cvgcmp2nlemabs  15763