Theorem eqidd 2239

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cbvraldva  2795  cbvrexdva  2796  rspcedeq1vd  2939  rspcedeq2vd  2940  nelrdva  3033  opeq2  3905  mpteq1  4215  tfisi  4734  feq23d  5529  f10d  5675  fvmptdv2  5795  elrnrexdm  5847  fmptco  5874  cofmpt  5877  ftpg  5899  fliftfun  6002  fliftval  6006  cbvmpo  6167  fconstmpo  6183  eqfnov2  6196  ovmpod  6216  ovmpodv2  6222  fvmpopr2d  6225  elovmporab  6289  elovmporab1w  6290  ofvalg  6312  ofrval  6313  off  6315  ofres  6317  suppssof1  6320  ofco  6321  caofref  6327  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  caofrss  6334  caoftrn  6335  uchoice  6371  suppofss1dcl  6504  suppofss2dcl  6505  rdgivallem  6652  iserd  6833  ixpsnf1o  7018  modom  7108  1domsn  7115  mapxpen  7148  infnninf  7464  ctssexmid  7490  nninfdcinf  7511  nninfwlporlemd  7512  nninfwlporlem  7513  nninfwlpoimlemginf  7516  nninfinfwlpo  7520  ofnegsub  9293  infrenegsupex  9996  fz0to4untppr  10533  fzo0to3tp  10639  modqsubmod  10821  0tonninf  10879  iseqovex  10897  seqvalcd  10900  seq3f1olemqsumkj  10950  seq3id  10964  seq3id2  10965  ccatws1ls  11412  pfxsuffeqwrdeq  11472  wrdind  11496  wrd2ind  11497  ccats1pfxeqbi  11516  s3eq2  11551  resqrexlemp1rp  11774  resqrexlemfp1  11777  resqrex  11794  infxrnegsupex  12031  climcl  12050  clim2  12051  climuni  12061  climeq  12067  2clim  12069  climshftlemg  12070  climabs0  12075  climcn1  12076  climcn2  12077  climge0  12093  climsqz  12103  climsqz2  12104  climcau  12115  climrecvg1n  12116  climcaucn  12119  serf0  12120  fzf1o  12144  isumz  12158  fisumss  12161  fsumsplitsn  12179  fsumsplitsnun  12188  isumclim3  12192  isummulc2  12195  fsum2dlemstep  12203  fsumconst  12223  fsumabs  12234  fsumparts  12239  iserabs  12244  fsumiun  12246  isumshft  12259  cvgratnnlemseq  12295  mertenslemub  12303  mertenslemi1  12304  mertenslem2  12305  prod1dc  12355  fprodssdc  12359  fprodunsn  12373  fprodcl2lem  12374  fprodconst  12389  fprod2dlemstep  12391  fprodsplitsn  12402  eftlcl  12457  reeftlcl  12458  eftlub  12459  efsep  12460  effsumlt  12461  eirraplem  12546  2tp1odd  12653  bezoutlemstep  12776  nninfctlemfo  12819  alginv  12827  algfx  12832  cncongr1  12883  qnumdencoprm  12973  qeqnumdivden  12974  ballotfilemgun  13270  ballotfilemfg  13271  ballotfilemfrc  13272  ctiunctal  13334  unct  13335  nninfdclemcl  13341  nninfdclemf  13342  nninfdclemp1  13343  nninfdc  13346  ressbasid  13426  ressressg  13431  imasex  13628  imasbas  13630  imasplusg  13631  imasmulr  13632  qusin  13649  gzsumvalx  13711  gzsumfzval  13713  gzsum0  13715  gzsumval2  13716  issgrp  13720  sgrp1  13728  issgrpd  13729  ismndd  13752  mndprop  13756  ress0g  13758  imasmnd2  13761  insubm  13794  resmhm  13796  resmhm2  13797  resmhm2b  13798  grpprop  13825  grpsubfvalg  13852  grpressid  13868  grpsubpropdg  13911  imasgrp2  13915  imasgrp  13916  imasgrpf1  13917  mulgfvalg  13926  mulgnngzsum  13932  mulgpropdg  13969  submmulg  13971  subginv  13986  subgcl  13989  subgsub  13991  releqgg  14025  eqgex  14026  eqgfval  14027  qusgrp  14037  resghm  14065  ablprop  14102  cmnsubm  14114  subcmnd  14139  ablressid  14141  gzsumconst  14145  gzsumconstf  14146  gzsummhm2  14148  gzsumsplit0  14150  gzsumshift  14151  gsumvalfi  14154  gzsumgsum  14157  gsumsncmn  14158  gsumzfi  14160  gsummhm2fi  14167  prdsex  14174  prdsbaslemss  14176  prdssca  14177  prdsbas  14178  prdsplusg  14179  prdsmulr  14180  prdssgrpd  14193  prdsmndd  14196  prdsgrpd  14199  isrng  14235  isrngd  14254  rngressid  14255  imasrng  14257  issrg  14271  srgidmlem  14284  isring  14306  ringass  14322  ringidmlem  14329  ringabl  14339  ringprop  14347  isringd  14348  ring1  14366  ringressid  14370  imasring  14371  opprrng  14384  opprring  14386  opprringbg  14387  opprsubgg  14392  mulgass3  14393  dvdsrcld  14406  dvdsrex  14407  dvdsrcl2  14408  dvdsrid  14409  dvdsrtr  14410  dvdsrneg  14412  dvdsr01  14413  1unit  14416  unitcld  14417  opprunitd  14419  crngunit  14420  unitmulcl  14422  unitgrpbasd  14424  unitgrp  14425  unitabl  14426  unitgrpid  14427  unitsubm  14428  unitlinv  14435  unitrinv  14436  unitnegcl  14439  dvrfvald  14442  dvrvald  14443  dvrcl  14444  unitdvcl  14445  dvrid  14446  dvr1  14447  dvrdir  14452  rdivmuldivd  14453  dvdsrpropdg  14456  unitpropdg  14457  invrpropdg  14458  rhmf1o  14477  rhmdvdsr  14484  elrhmunit  14486  rhmunitinv  14487  opprlring  14506  issubrng2  14520  subrngpropd  14526  subrgcrng  14535  subrgdvds  14545  subrguss  14546  subrginv  14547  subrgdv  14548  subrgunit  14549  subrgugrp  14550  issubrg2  14551  subrgpropd  14563  aprunit  14594  aprirr  14597  aprsym  14598  aprcotr  14599  aprap  14600  aprnzr  14601  aprlring  14602  aprprop  14603  opprdrng  14622  islmodd  14631  lmodabl  14673  lss1  14701  lsssn0  14709  islss3  14718  lss1d  14722  lssintclm  14723  lsslsp  14768  sralmod  14789  sralmod0g  14790  rlmfn  14792  rlmvalg  14793  rlm0g  14796  rlmvnegg  14804  lidlssbas  14816  islidlm  14818  rnglidlmsgrp  14836  rnglidlrng  14837  qus2idrng  14864  crngridl  14869  quscrng  14872  cnfldui  14926  dvdsrzring  14940  zrhpropd  14963  znzrh  14980  znbas  14981  zncrng  14982  znzrhfo  14985  znf1o  14988  znunit  14996  isassad  15013  issubassa3  15014  asclfval  15023  ressascl  15041  psrval  15052  psrbaglesuppg  15059  psrbagcon  15064  psrbagconf1o  15066  psrbasg  15067  psrplusgg  15071  mplsubgfilemcl  15092  mplplusgg  15096  epttop  15193  lmss  15349  txlm  15382  lmcn2  15383  cnmpt2c  15393  txswaphmeolem  15423  blfvalps  15488  bdxmet  15604  mpomulcn  15669  fsumcncntop  15670  cncfmptc  15699  cncfmpt1f  15701  cdivcncfap  15707  negfcncf  15709  divcncfap  15717  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dviaddf  15808  dvexp  15814  dvmptaddx  15822  dvmptmulx  15823  dvmptfsum  15828  dvef  15830  elply2  15838  elplyr  15843  plyaddlem1  15850  plycolemc  15861  sincn  15872  coscn  15873  logfac  16001  lgsdir2lem5  16163  gausslemma2dlem1  16192  lgseisenlem2  16202  lgseisenlem3  16203  lgseisenlem4  16204  lgsquad2lem2  16213  2lgslem1b  16220  2lgslem3b1  16229  2lgslem3c1  16230  2lgsoddprmlem4  16243  2sqlem8  16254  usgredg4  16468  ushgredgedg  16479  ushgredgedgloop  16481  usgrstrrepeen  16484  uspgr1edc  16493  wlk1walkdom  16612  uspgr2wlkeq  16618  uspgr2wlkeqi  16620  clwwlknonmpo  16681  iseupth  16700  eupth2lem2dc  16712  konigsberglem2  16742  konigsberglem3  16743  nninfsellemeqinf  17071  nninffeq  17075  nnnninfex  17077  exmidsbthrlem  17079  cvgcmp2nlemabs  17093