Theorem eqidd 2235

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

Syntax hints:   → wi 4   = wceq 1398

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 1498  ax-ext 2216

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

This theorem is referenced by:  cbvraldva  2789  cbvrexdva  2790  rspcedeq1vd  2933  rspcedeq2vd  2934  nelrdva  3027  opeq2  3889  mpteq1  4199  tfisi  4714  feq23d  5509  f10d  5655  fvmptdv2  5772  elrnrexdm  5821  fmptco  5848  cofmpt  5851  ftpg  5873  fliftfun  5975  fliftval  5979  cbvmpo  6140  fconstmpo  6156  eqfnov2  6169  ovmpod  6189  ovmpodv2  6195  fvmpopr2d  6198  elovmporab  6262  elovmporab1w  6263  ofvalg  6285  ofrval  6286  off  6288  ofres  6290  suppssof1  6293  ofco  6294  caofref  6300  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  caofrss  6307  caoftrn  6308  uchoice  6344  suppofss1dcl  6477  suppofss2dcl  6478  rdgivallem  6625  iserd  6806  ixpsnf1o  6984  modom  7074  1domsn  7081  mapxpen  7114  infnninf  7428  ctssexmid  7454  nninfdcinf  7475  nninfwlporlemd  7476  nninfwlporlem  7477  nninfwlpoimlemginf  7480  nninfinfwlpo  7484  ofnegsub  9256  infrenegsupex  9947  fz0to4untppr  10483  fzo0to3tp  10589  modqsubmod  10771  0tonninf  10829  iseqovex  10847  seqvalcd  10850  seq3f1olemqsumkj  10900  seq3id  10914  seq3id2  10915  ccatws1ls  11358  pfxsuffeqwrdeq  11418  wrdind  11442  wrd2ind  11443  ccats1pfxeqbi  11462  s3eq2  11497  resqrexlemp1rp  11720  resqrexlemfp1  11723  resqrex  11740  infxrnegsupex  11977  climcl  11996  clim2  11997  climuni  12007  climeq  12013  2clim  12015  climshftlemg  12016  climabs0  12021  climcn1  12022  climcn2  12023  climge0  12039  climsqz  12049  climsqz2  12050  climcau  12061  climrecvg1n  12062  climcaucn  12065  serf0  12066  fzf1o  12090  isumz  12104  fisumss  12107  fsumsplitsn  12125  fsumsplitsnun  12134  isumclim3  12138  isummulc2  12141  fsum2dlemstep  12149  fsumconst  12169  fsumabs  12180  fsumparts  12185  iserabs  12190  fsumiun  12192  isumshft  12205  cvgratnnlemseq  12241  mertenslemub  12249  mertenslemi1  12250  mertenslem2  12251  prod1dc  12301  fprodssdc  12305  fprodunsn  12319  fprodcl2lem  12320  fprodconst  12335  fprod2dlemstep  12337  fprodsplitsn  12348  eftlcl  12403  reeftlcl  12404  eftlub  12405  efsep  12406  effsumlt  12407  eirraplem  12492  2tp1odd  12599  bezoutlemstep  12722  nninfctlemfo  12765  alginv  12773  algfx  12778  cncongr1  12829  qnumdencoprm  12919  qeqnumdivden  12920  ballotfilemgun  13216  ballotfilemfg  13217  ballotfilemfrc  13218  ctiunctal  13280  unct  13281  nninfdclemcl  13287  nninfdclemf  13288  nninfdclemp1  13289  nninfdc  13292  ressbasid  13371  ressressg  13376  imasex  13573  imasbas  13575  imasplusg  13576  imasmulr  13577  qusin  13594  igsumvalx  13656  gsumfzval  13658  gsumpropd  13659  gsumpropd2  13660  gsum0g  13663  gsumval2  13664  issgrp  13670  sgrp1  13678  issgrpd  13679  ismndd  13702  mndprop  13706  ress0g  13708  imasmnd2  13711  insubm  13744  resmhm  13746  resmhm2  13747  resmhm2b  13748  gsumfzz  13754  grpprop  13777  grpsubfvalg  13804  grpressid  13820  grpsubpropdg  13863  imasgrp2  13867  imasgrp  13868  imasgrpf1  13869  mulgfvalg  13878  mulgnngsum  13884  mulgpropdg  13921  submmulg  13923  subginv  13938  subgcl  13941  subgsub  13943  releqgg  13977  eqgex  13978  eqgfval  13979  qusgrp  13989  resghm  14017  ablprop  14054  subcmnd  14090  ablressid  14092  gsumfzmptfidmadd  14096  gsumfzconst  14098  gsumfzconstf  14099  gsumfzmhm2  14101  gsumsplit0  14103  gfsumval  14106  gsumshift  14109  gsumgfsum  14110  gfsumsn  14111  gfsumz  14113  prdsex  14118  prdsbaslemss  14120  prdssca  14121  prdsbas  14122  prdsplusg  14123  prdsmulr  14124  prdssgrpd  14137  prdsmndd  14140  prdsgrpd  14143  isrng  14177  isrngd  14196  rngressid  14197  imasrng  14199  issrg  14212  srgidmlem  14225  isring  14247  ringass  14263  ringidmlem  14269  ringabl  14279  ringprop  14287  isringd  14288  ring1  14306  ringressid  14310  imasring  14311  opprrng  14324  opprring  14326  opprringbg  14327  opprsubgg  14332  mulgass3  14333  dvdsrcld  14346  dvdsrex  14347  dvdsrcl2  14348  dvdsrid  14349  dvdsrtr  14350  dvdsrneg  14352  dvdsr01  14353  1unit  14356  unitcld  14357  opprunitd  14359  crngunit  14360  unitmulcl  14362  unitgrpbasd  14364  unitgrp  14365  unitabl  14366  unitgrpid  14367  unitsubm  14368  unitlinv  14375  unitrinv  14376  unitnegcl  14379  dvrfvald  14382  dvrvald  14383  dvrcl  14384  unitdvcl  14385  dvrid  14386  dvr1  14387  dvrdir  14392  rdivmuldivd  14393  dvdsrpropdg  14396  unitpropdg  14397  invrpropdg  14398  rhmf1o  14417  rhmdvdsr  14424  elrhmunit  14426  rhmunitinv  14427  opprlring  14446  issubrng2  14460  subrngpropd  14466  subrgcrng  14475  subrgdvds  14485  subrguss  14486  subrginv  14487  subrgdv  14488  subrgunit  14489  subrgugrp  14490  issubrg2  14491  subrgpropd  14503  aprunit  14534  aprirr  14537  aprsym  14538  aprcotr  14539  aprap  14540  aprnzr  14541  aprlring  14542  aprprop  14543  opprdrng  14562  islmodd  14571  lmodabl  14612  lss1  14640  lsssn0  14648  islss3  14657  lss1d  14661  lssintclm  14662  lsslsp  14707  sralmod  14728  sralmod0g  14729  rlmfn  14731  rlmvalg  14732  rlm0g  14735  rlmvnegg  14743  lidlssbas  14755  islidlm  14757  rnglidlmsgrp  14775  rnglidlrng  14776  qus2idrng  14803  crngridl  14808  quscrng  14811  cnfldui  14867  dvdsrzring  14881  zrhpropd  14904  znzrh  14921  znbas  14922  zncrng  14923  znzrhfo  14926  znf1o  14929  znunit  14937  psrval  14944  psrbaglesuppg  14951  psrbagcon  14956  psrbagconf1o  14958  psrbasg  14959  psrplusgg  14963  mplsubgfilemcl  14984  mplplusgg  14988  epttop  15085  lmss  15241  txlm  15274  lmcn2  15275  cnmpt2c  15285  txswaphmeolem  15315  blfvalps  15380  bdxmet  15496  mpomulcn  15561  fsumcncntop  15562  cncfmptc  15591  cncfmpt1f  15593  cdivcncfap  15599  negfcncf  15601  divcncfap  15609  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvcnp2cntop  15694  dvaddxxbr  15696  dvmulxxbr  15697  dviaddf  15700  dvexp  15706  dvmptaddx  15714  dvmptmulx  15715  dvmptfsum  15720  dvef  15722  elply2  15730  elplyr  15735  plyaddlem1  15742  plycolemc  15753  sincn  15764  coscn  15765  lgsdir2lem5  16035  gausslemma2dlem1  16064  lgseisenlem2  16074  lgseisenlem3  16075  lgseisenlem4  16076  lgsquad2lem2  16085  2lgslem1b  16092  2lgslem3b1  16101  2lgslem3c1  16102  2lgsoddprmlem4  16115  2sqlem8  16126  usgredg4  16340  ushgredgedg  16351  ushgredgedgloop  16353  usgrstrrepeen  16356  uspgr1edc  16365  wlk1walkdom  16484  uspgr2wlkeq  16490  uspgr2wlkeqi  16492  clwwlknonmpo  16553  iseupth  16572  eupth2lem2dc  16584  konigsberglem2  16614  konigsberglem3  16615  nninfsellemeqinf  16934  nninffeq  16938  nnnninfex  16940  exmidsbthrlem  16942  cvgcmp2nlemabs  16956