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  ofrfidc  7318  infnninf  7465  ctssexmid  7491  nninfdcinf  7512  nninfwlporlemd  7513  nninfwlporlem  7514  nninfwlpoimlemginf  7517  nninfinfwlpo  7521  ofnegsub  9295  infrenegsupex  10004  fz0to4untppr  10542  fzo0to3tp  10648  modqsubmod  10833  0tonninf  10891  iseqovex  10909  seqvalcd  10912  seq3f1olemqsumkj  10962  seq3id  10976  seq3id2  10977  ccatws1ls  11425  pfxsuffeqwrdeq  11485  wrdind  11509  wrd2ind  11510  ccats1pfxeqbi  11529  s3eq2  11564  resqrexlemp1rp  11787  resqrexlemfp1  11790  resqrex  11807  infxrnegsupex  12047  climcl  12066  clim2  12067  climuni  12077  climeq  12083  2clim  12085  climshftlemg  12086  climabs0  12091  climcn1  12092  climcn2  12093  climge0  12109  climsqz  12119  climsqz2  12120  climcau  12131  climrecvg1n  12132  climcaucn  12135  serf0  12136  fzf1o  12160  isumz  12174  fisumss  12177  fsumsplitsn  12195  fsumsplitsnun  12204  isumclim3  12208  isummulc2  12211  fsum2dlemstep  12219  fsumconst  12239  fsumabs  12250  fsumparts  12255  iserabs  12260  fsumiun  12262  isumshft  12275  cvgratnnlemseq  12311  mertenslemub  12319  mertenslemi1  12320  mertenslem2  12321  prod1dc  12371  fprodssdc  12375  fprodunsn  12389  fprodcl2lem  12390  fprodconst  12405  fprod2dlemstep  12407  fprodsplitsn  12418  eftlcl  12473  reeftlcl  12474  eftlub  12475  efsep  12476  effsumlt  12477  eirraplem  12562  2tp1odd  12669  bezoutlemstep  12792  nninfctlemfo  12835  alginv  12843  algfx  12848  cncongr1  12899  qnumdencoprm  12991  qeqnumdivden  12992  ballotfilemgun  13319  ballotfilemfg  13320  ballotfilemfrc  13321  ctiunctal  13383  unct  13384  nninfdclemcl  13390  nninfdclemf  13391  nninfdclemp1  13392  nninfdc  13395  ressbasid  13475  ressressg  13480  imasex  13677  imasbas  13679  imasplusg  13680  imasmulr  13681  qusin  13698  gzsumvalx  13760  gzsumfzval  13762  gzsum0  13764  gzsumval2  13765  issgrp  13769  sgrp1  13777  issgrpd  13778  ismndd  13801  mndprop  13805  ress0g  13807  imasmnd2  13810  insubm  13843  resmhm  13845  resmhm2  13846  resmhm2b  13847  grpprop  13874  grpsubfvalg  13901  grpressid  13917  grpsubpropdg  13960  imasgrp2  13964  imasgrp  13965  imasgrpf1  13966  mulgfvalg  13975  mulgnngzsum  13981  mulgpropdg  14018  submmulg  14020  subginv  14035  subgcl  14038  subgsub  14040  releqgg  14074  eqgex  14075  eqgfval  14076  qusgrp  14086  resghm  14114  ablprop  14151  cmnsubm  14163  subcmnd  14188  ablressid  14190  gzsumconst  14194  gzsumconstf  14195  gzsummhm2  14197  gzsumsplit0  14199  gzsumshift  14200  gsumvalfi  14203  gzsumgsum  14206  gsumsncmn  14207  gsumzfi  14209  gsummhm2fi  14216  prdsex  14223  prdsbaslemss  14225  prdssca  14226  prdsbas  14227  prdsplusg  14228  prdsmulr  14229  prdssgrpd  14242  prdsmndd  14245  prdsgrpd  14248  isrng  14284  isrngd  14303  rngressid  14304  imasrng  14306  issrg  14320  srgidmlem  14333  isring  14355  ringass  14371  ringidmlem  14378  ringabl  14388  ringprop  14396  isringd  14397  ring1  14415  ringressid  14419  imasring  14420  opprrng  14433  opprring  14435  opprringbg  14436  opprsubgg  14441  mulgass3  14442  dvdsrcld  14455  dvdsrex  14456  dvdsrcl2  14457  dvdsrid  14458  dvdsrtr  14459  dvdsrneg  14461  dvdsr01  14462  1unit  14465  unitcld  14466  opprunitd  14468  crngunit  14469  unitmulcl  14471  unitgrpbasd  14473  unitgrp  14474  unitabl  14475  unitgrpid  14476  unitsubm  14477  unitlinv  14484  unitrinv  14485  unitnegcl  14488  dvrfvald  14491  dvrvald  14492  dvrcl  14493  unitdvcl  14494  dvrid  14495  dvr1  14496  dvrdir  14501  rdivmuldivd  14502  dvdsrpropdg  14505  unitpropdg  14506  invrpropdg  14507  rhmf1o  14526  rhmdvdsr  14533  elrhmunit  14535  rhmunitinv  14536  opprlring  14555  issubrng2  14569  subrngpropd  14575  subrgcrng  14584  subrgdvds  14594  subrguss  14595  subrginv  14596  subrgdv  14597  subrgunit  14598  subrgugrp  14599  issubrg2  14600  subrgpropd  14612  aprunit  14643  aprirr  14646  aprsym  14647  aprcotr  14648  aprap  14649  aprnzr  14650  aprlring  14651  aprprop  14652  opprdrng  14671  islmodd  14680  lmodabl  14722  lss1  14750  lsssn0  14758  islss3  14767  lss1d  14771  lssintclm  14772  lsslsp  14817  sralmod  14838  sralmod0g  14839  rlmfn  14841  rlmvalg  14842  rlm0g  14845  rlmvnegg  14853  lidlssbas  14865  islidlm  14867  rnglidlmsgrp  14885  rnglidlrng  14886  qus2idrng  14913  crngridl  14918  quscrng  14921  cnfldui  14975  dvdsrzring  14989  zrhpropd  15012  znzrh  15029  znbas  15030  zncrng  15031  znzrhfo  15034  znf1o  15037  znunit  15045  isassad  15062  issubassa3  15063  asclfval  15072  ressascl  15090  psrval  15101  psrbaglesuppg  15108  psrbagcon  15113  psrbaglefifi  15114  psrbagconf1o  15116  psrbasg  15117  psrplusgg  15121  mplsubgfilemcl  15142  mplplusgg  15146  epttop  15243  lmss  15399  txlm  15432  lmcn2  15433  cnmpt2c  15443  txswaphmeolem  15473  blfvalps  15538  bdxmet  15654  mpomulcn  15719  fsumcncntop  15720  cncfmptc  15749  cncfmpt1f  15751  cdivcncfap  15757  negfcncf  15759  divcncfap  15767  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvcnp2cntop  15852  dvaddxxbr  15854  dvmulxxbr  15855  dviaddf  15858  dvexp  15864  dvmptaddx  15872  dvmptmulx  15873  dvmptfsum  15878  dvef  15880  elply2  15888  elplyr  15893  plyaddlem1  15900  plycolemc  15911  sincn  15922  coscn  15923  logfac  16051  chtublem  16217  lgsdir2lem5  16273  gausslemma2dlem1  16302  lgseisenlem2  16312  lgseisenlem3  16313  lgseisenlem4  16314  lgsquad2lem2  16323  2lgslem1b  16330  2lgslem3b1  16339  2lgslem3c1  16340  2lgsoddprmlem4  16353  2sqlem8  16364  usgredg4  16578  ushgredgedg  16589  ushgredgedgloop  16591  usgrstrrepeen  16594  uspgr1edc  16603  wlk1walkdom  16722  uspgr2wlkeq  16728  uspgr2wlkeqi  16730  clwwlknonmpo  16791  iseupth  16810  eupth2lem2dc  16822  konigsberglem2  16852  konigsberglem3  16853  nninfsellemeqinf  17181  nninffeq  17185  nnnninfex  17187  exmidsbthrlem  17189  cvgcmp2nlemabs  17203