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  4216  mpteq1i  4218  tfisi  4736  feq23d  5532  f10d  5678  fvmptdv2  5798  elrnrexdm  5850  fmptco  5877  cofmpt  5880  ftpg  5902  fliftfun  6005  fliftval  6009  cbvmpo  6170  fconstmpo  6186  eqfnov2  6199  ovmpod  6219  ovmpodv2  6225  fvmpopr2d  6228  elovmporab  6292  elovmporab1w  6293  ofvalg  6316  ofrval  6317  off  6319  ofres  6321  suppssof1  6324  ofco  6325  caofref  6331  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  caofrss  6338  caoftrn  6339  uchoice  6375  suppofss1dcl  6508  suppofss2dcl  6509  rdgivallem  6656  iserd  6837  ixpsnf1o  7022  modom  7112  1domsn  7119  mapxpen  7152  ofrfidc  7323  infnninf  7470  ctssexmid  7496  nninfdcinf  7517  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemginf  7522  nninfinfwlpo  7526  ofsubeq0  9300  ofnegsub  9301  infrenegsupex  10010  fz0to4untppr  10548  fzo0to3tp  10654  modqsubmod  10840  0tonninf  10898  iseqovex  10916  seqvalcd  10919  seq3f1olemqsumkj  10969  seq3id  10983  seq3id2  10984  ccatws1ls  11432  pfxsuffeqwrdeq  11492  wrdind  11516  wrd2ind  11517  ccats1pfxeqbi  11536  s3eq2  11571  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrex  11814  infxrnegsupex  12054  climcl  12073  clim2  12074  climuni  12084  climeq  12090  2clim  12092  climshftlemg  12093  climabs0  12098  climcn1  12099  climcn2  12100  climge0  12116  climsqz  12126  climsqz2  12127  climcau  12138  climrecvg1n  12139  climcaucn  12142  serf0  12143  fzf1o  12167  isumz  12181  fisumss  12184  fsumsplitsn  12202  fsumsplitsnun  12211  isumclim3  12215  isummulc2  12218  fsum2dlemstep  12226  fsumconst  12246  fsumabs  12257  fsumparts  12262  iserabs  12267  fsumiun  12269  isumshft  12282  cvgratnnlemseq  12318  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  prod1dc  12378  fprodssdc  12382  fprodunsn  12396  fprodcl2lem  12397  fprodconst  12412  fprod2dlemstep  12414  fprodsplitsn  12425  eftlcl  12480  reeftlcl  12481  eftlub  12482  efsep  12483  effsumlt  12484  eirraplem  12569  2tp1odd  12676  bezoutlemstep  12799  nninfctlemfo  12842  alginv  12850  algfx  12855  cncongr1  12906  qnumdencoprm  12998  qeqnumdivden  12999  ballotfilemgun  13326  ballotfilemfg  13327  ballotfilemfrc  13328  ctiunctal  13390  unct  13391  nninfdclemcl  13397  nninfdclemf  13398  nninfdclemp1  13399  nninfdc  13402  ressbasid  13483  ressressg  13488  imasex  13685  imasbas  13687  imasplusg  13688  imasmulr  13689  qusin  13706  gzsumvalx  13768  gzsumfzval  13770  gzsum0  13772  gzsumval2  13773  issgrp  13777  sgrp1  13785  issgrpd  13786  ismndd  13809  mndprop  13813  ress0g  13815  imasmnd2  13818  insubm  13851  resmhm  13853  resmhm2  13854  resmhm2b  13855  grpprop  13882  grpsubfvalg  13909  grpressid  13925  grpsubpropdg  13968  imasgrp2  13972  imasgrp  13973  imasgrpf1  13974  mulgfvalg  13983  mulgnngzsum  13989  mulgpropdg  14026  submmulg  14028  subginv  14043  subgcl  14046  subgsub  14048  releqgg  14082  eqgex  14083  eqgfval  14084  qusgrp  14094  resghm  14122  resscntz  14166  ablprop  14190  cmnsubm  14202  subcmnd  14227  ablressid  14229  gzsumconst  14233  gzsumconstf  14234  gzsummhm2  14236  gzsumsplit0  14238  gzsumshift  14239  gsumvalfi  14242  gzsumgsum  14245  gsumsncmn  14246  gsumzfi  14248  gsumunsnfd  14259  gsummhm2fi  14265  gsum2dfilem2  14272  gsumcom2fi  14275  prdsex  14279  prdsbaslemss  14281  prdssca  14282  prdsbas  14283  prdsplusg  14284  prdsmulr  14285  prdssgrpd  14298  prdsmndd  14301  prdsgrpd  14304  isrng  14340  isrngd  14359  rngressid  14360  imasrng  14362  issrg  14376  srgidmlem  14389  isring  14411  ringass  14427  ringidmlem  14434  ringabl  14444  ringprop  14452  isringd  14453  ring1  14471  ringressid  14477  imasring  14478  opprrng  14491  opprring  14493  opprringbg  14494  opprsubgg  14499  mulgass3  14500  dvdsrcld  14513  dvdsrex  14514  dvdsrcl2  14515  dvdsrid  14516  dvdsrtr  14517  dvdsrneg  14519  dvdsr01  14520  1unit  14523  unitcld  14524  opprunitd  14526  crngunit  14527  unitmulcl  14529  unitgrpbasd  14531  unitgrp  14532  unitabl  14533  unitgrpid  14534  unitsubm  14535  unitlinv  14542  unitrinv  14543  unitnegcl  14546  dvrfvald  14549  dvrvald  14550  dvrcl  14551  unitdvcl  14552  dvrid  14553  dvr1  14554  dvrdir  14559  rdivmuldivd  14560  dvdsrpropdg  14563  unitpropdg  14564  invrpropdg  14565  rhmf1o  14584  rhmdvdsr  14591  elrhmunit  14593  rhmunitinv  14594  opprlring  14613  issubrng2  14627  subrngpropd  14633  subrgcrng  14642  subrgdvds  14652  subrguss  14653  subrginv  14654  subrgdv  14655  subrgunit  14656  subrgugrp  14657  issubrg2  14658  subrgpropd  14670  aprunit  14701  aprirr  14704  aprsym  14705  aprcotr  14706  aprap  14707  aprnzr  14708  aprlring  14709  aprprop  14710  opprdrng  14729  islmodd  14738  lmodabl  14780  lss1  14808  lsssn0  14816  islss3  14825  lss1d  14829  lssintclm  14830  lsslsp  14875  sralmod  14896  sralmod0g  14897  rlmfn  14899  rlmvalg  14900  rlm0g  14903  rlmvnegg  14911  lidlssbas  14923  islidlm  14925  rnglidlmsgrp  14943  rnglidlrng  14944  qus2idrng  14971  crngridl  14976  quscrng  14979  cnfldui  15033  dvdsrzring  15047  zrhpropd  15070  znzrh  15087  znbas  15088  zncrng  15089  znzrhfo  15092  znf1o  15095  znunit  15103  isassad  15120  issubassa3  15121  asclfval  15130  ressascl  15148  psrval  15159  psrbaglesuppg  15166  psrbagcon  15171  psrbaglefifi  15172  psrbagconf1o  15174  gsumbagdiaglem  15175  psrass1filem  15177  psrbasg  15178  psrplusgg  15182  psrmulrg  15186  psrlidmfi  15199  psrdifi  15202  psrdirfi  15203  psrringfi  15204  mplsubgfilemcl  15215  mplplusgg  15219  epttop  15316  lmss  15472  txlm  15505  lmcn2  15506  cnmpt2c  15516  txswaphmeolem  15546  blfvalps  15611  bdxmet  15727  mpomulcn  15792  fsumcncntop  15793  cncfmptc  15822  cncfmpt1f  15824  cdivcncfap  15830  negfcncf  15832  divcncfap  15840  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dviaddf  15931  dvexp  15937  dvmptaddx  15945  dvmptmulx  15946  dvmptfsum  15951  dvef  15953  elply2  15961  elplyr  15966  plyaddlem1  15973  plycolemc  15984  sincn  15995  coscn  15996  logfac  16126  chtublem  16295  bposlem6  16316  lgsdir2lem5  16356  gausslemma2dlem1  16385  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquad2lem2  16406  2lgslem1b  16413  2lgslem3b1  16422  2lgslem3c1  16423  2lgsoddprmlem4  16436  2sqlem8  16447  usgredg4  16661  ushgredgedg  16672  ushgredgedgloop  16674  usgrstrrepeen  16677  uspgr1edc  16686  wlk1walkdom  16805  uspgr2wlkeq  16811  uspgr2wlkeqi  16813  clwwlknonmpo  16874  iseupth  16893  eupth2lem2dc  16905  konigsberglem2  16935  konigsberglem3  16936  nninfsellemeqinf  17265  nninffeq  17269  nnnninfex  17271  exmidsbthrlem  17273  cvgcmp2nlemabs  17287