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  5404  fvmptdv2  5652  elrnrexdm  5702  fmptco  5729  cofmpt  5732  ftpg  5747  fliftfun  5844  fliftval  5848  cbvmpo  6003  fconstmpo  6019  eqfnov2  6032  ovmpod  6052  ovmpodv2  6058  fvmpopr2d  6061  elovmporab  6125  elovmporab1w  6126  ofvalg  6147  ofrval  6148  off  6150  ofres  6152  suppssof1  6155  ofco  6156  caofref  6161  caofrss  6164  caoftrn  6165  uchoice  6197  rdgivallem  6441  iserd  6620  ixpsnf1o  6797  1domsn  6880  mapxpen  6911  infnninf  7192  ctssexmid  7218  nninfdcinf  7239  nninfwlporlemd  7240  nninfwlporlem  7241  nninfwlpoimlemginf  7244  ofnegsub  8992  infrenegsupex  9671  fz0to4untppr  10202  fzo0to3tp  10298  modqsubmod  10477  0tonninf  10535  iseqovex  10553  seqvalcd  10556  seq3f1olemqsumkj  10606  seq3id  10620  seq3id2  10621  resqrexlemp1rp  11174  resqrexlemfp1  11177  resqrex  11194  infxrnegsupex  11431  climcl  11450  clim2  11451  climuni  11461  climeq  11467  2clim  11469  climshftlemg  11470  climabs0  11475  climcn1  11476  climcn2  11477  climge0  11493  climsqz  11503  climsqz2  11504  climcau  11515  climrecvg1n  11516  climcaucn  11519  serf0  11520  isumz  11557  fisumss  11560  fsumsplitsn  11578  fsumsplitsnun  11587  isumclim3  11591  isummulc2  11594  fsum2dlemstep  11602  fsumconst  11622  fsumabs  11633  fsumparts  11638  iserabs  11643  fsumiun  11645  isumshft  11658  cvgratnnlemseq  11694  mertenslemub  11702  mertenslemi1  11703  mertenslem2  11704  prod1dc  11754  fprodssdc  11758  fprodunsn  11772  fprodcl2lem  11773  fprodconst  11788  fprod2dlemstep  11790  fprodsplitsn  11801  eftlcl  11856  reeftlcl  11857  eftlub  11858  efsep  11859  effsumlt  11860  eirraplem  11945  2tp1odd  12052  bezoutlemstep  12175  nninfctlemfo  12218  alginv  12226  algfx  12231  cncongr1  12282  qnumdencoprm  12372  qeqnumdivden  12373  ctiunctal  12669  unct  12670  nninfdclemcl  12676  nninfdclemf  12677  nninfdclemp1  12678  nninfdc  12681  ressbasid  12759  ressressg  12764  prdsex  12957  prdsbaslemss  12962  prdssca  12963  prdsbas  12964  prdsplusg  12965  prdsmulr  12966  imasex  12974  imasbas  12976  imasplusg  12977  imasmulr  12978  qusin  12995  igsumvalx  13058  gsumfzval  13060  gsumpropd  13061  gsumpropd2  13062  gsum0g  13065  gsumval2  13066  issgrp  13072  sgrp1  13080  issgrpd  13081  ismndd  13104  mndprop  13108  ress0g  13110  insubm  13143  resmhm  13145  resmhm2  13146  resmhm2b  13147  gsumfzz  13153  grpprop  13176  grpsubfvalg  13203  grpressid  13219  grpsubpropdg  13262  imasgrp2  13266  imasgrp  13267  imasgrpf1  13268  mulgfvalg  13277  mulgnngsum  13283  mulgpropdg  13320  submmulg  13322  subginv  13337  subgcl  13340  subgsub  13342  releqgg  13376  eqgex  13377  eqgfval  13378  qusgrp  13388  resghm  13416  ablprop  13453  subcmnd  13489  ablressid  13491  gsumfzmptfidmadd  13495  gsumfzconst  13497  gsumfzconstf  13498  gsumfzmhm2  13500  isrng  13516  isrngd  13535  rngressid  13536  imasrng  13538  issrg  13547  srgidmlem  13560  isring  13582  ringass  13598  ringidmlem  13604  ringabl  13614  ringprop  13622  isringd  13623  ring1  13641  ringressid  13645  imasring  13646  opprrng  13659  opprring  13661  opprringbg  13662  opprsubgg  13666  mulgass3  13667  dvdsrcld  13679  dvdsrex  13680  dvdsrcl2  13681  dvdsrid  13682  dvdsrtr  13683  dvdsrneg  13685  dvdsr01  13686  1unit  13689  unitcld  13690  opprunitd  13692  crngunit  13693  unitmulcl  13695  unitgrpbasd  13697  unitgrp  13698  unitabl  13699  unitgrpid  13700  unitsubm  13701  unitlinv  13708  unitrinv  13709  unitnegcl  13712  dvrfvald  13715  dvrvald  13716  dvrcl  13717  unitdvcl  13718  dvrid  13719  dvr1  13720  dvrdir  13725  rdivmuldivd  13726  dvdsrpropdg  13729  unitpropdg  13730  invrpropdg  13731  rhmf1o  13750  rhmdvdsr  13757  elrhmunit  13759  rhmunitinv  13760  issubrng2  13792  subrngpropd  13798  subrgcrng  13807  subrgdvds  13817  subrguss  13818  subrginv  13819  subrgdv  13820  subrgunit  13821  subrgugrp  13822  issubrg2  13823  subrgpropd  13835  aprirr  13865  aprsym  13866  aprcotr  13867  aprap  13868  islmodd  13875  lmodabl  13916  lss1  13944  lsssn0  13952  islss3  13961  lss1d  13965  lssintclm  13966  lsslsp  14011  sralmod  14032  sralmod0g  14033  rlmfn  14035  rlmvalg  14036  rlm0g  14039  rlmvnegg  14047  lidlssbas  14059  islidlm  14061  rnglidlmsgrp  14079  rnglidlrng  14080  qus2idrng  14107  crngridl  14112  quscrng  14115  cnfldui  14171  dvdsrzring  14185  zrhpropd  14208  znzrh  14225  znbas  14226  zncrng  14227  znzrhfo  14230  znf1o  14233  znunit  14241  psrval  14246  psrbaglesuppg  14252  psrbasg  14253  psrplusgg  14256  epttop  14352  lmss  14508  txlm  14541  lmcn2  14542  cnmpt2c  14552  txswaphmeolem  14582  blfvalps  14647  bdxmet  14763  mpomulcn  14828  fsumcncntop  14829  cncfmptc  14858  cncfmpt1f  14860  cdivcncfap  14866  negfcncf  14868  divcncfap  14876  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dvcnp2cntop  14961  dvaddxxbr  14963  dvmulxxbr  14964  dviaddf  14967  dvexp  14973  dvmptaddx  14981  dvmptmulx  14982  dvmptfsum  14987  dvef  14989  elply2  14997  elplyr  15002  plyaddlem1  15009  plycolemc  15020  sincn  15031  coscn  15032  lgsdir2lem5  15299  gausslemma2dlem1  15328  lgseisenlem2  15338  lgseisenlem3  15339  lgseisenlem4  15340  lgsquad2lem2  15349  2lgslem1b  15356  2lgslem3b1  15365  2lgslem3c1  15366  2lgsoddprmlem4  15379  2sqlem8  15390  nninfsellemeqinf  15689  nninffeq  15693  exmidsbthrlem  15695  cvgcmp2nlemabs  15705