Theorem eqidd 1885

Description: Class identity law with antecedent.

Assertion

Ref	Expression
eqidd	|- (ph -> A = A)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 1884	. 2 |- A = A
2	1	a1i 8	1 |- (ph -> A = A)

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  1st2val 5038  2nd2val 5039  iotanul 5098  riotabidv 5562  hartoglem 5692  fsumconst 8298  climabs0i 8373  acdc3lem 8754  acdclem 8763  acdcALT 8765  txuni 8935  minveclem9 9898  oprabco 10159  upxp 10225  uptx 10226  txcn 10227  txcnopab 10228  subtopmet 10256  limfil 10297  iscom2 10396  opsqrlem4 11714  alginv 13743  algfx 13748  elno2 14005  eqfnung2 14459  cbicplem 14508  islatalg 14531  prodeq1 14658  fprodp1s1 14683  fincmpzer 14711  isppm 14715  fprodneg 14741  fprodsub 14742  vecval1b 14794  vecval3b 14795  vri 14834  idtrgrp 14978  cnvtr 15016  imonclem 15162  iepiclem 15172  cinvlem2 15177  partarelt2 15274  elfiun 15369  inficlALT 15372  hartoglemOLD 15383  subntr 15425  cnsubsp2 15427  hscptsscld 15434  connsub 15443  rnelfmlem 15592  rnelfm 15593  filclus 15605  unirep 15664  eqfnoprv2 15704  fnopabco 15711  upixp 15729  inficl 15757  seq1p1g 15805  seqzp1g 15807  sdclem1 15809  fdc 15812  lmclim2 15850  txsubsp 15912  totbndss 15937  totbndbnd 15944  heiborlem34 15988  bfplem3 16000  rrnmet 16016  rrncms 16019  rrntotbndlem1 16020  phtpyid 16049  phtpycolem4 16054  pcohtpylem3 16082  cmtfval 16937  isoml 16959  islvec 17188  paddfval 17258

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-cleq 1877

Copyright terms: Public domain