HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eqeltrd 1540
Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
eqeltrd.1 |- (ph -> A = B)
eqeltrd.2 |- (ph -> B e. C)
Assertion
Ref Expression
eqeltrd |- (ph -> A e. C)
Proof of Theorem eqeltrd
StepHypRef Expression
1 eqeltrd.2 . 2 |- (ph -> B e. C)
2 eqeltrd.1 . . 3 |- (ph -> A = B)
32eleq1d 1532 . 2 |- (ph -> (A e. C <-> B e. C))
41, 3mpbird 196 1 |- (ph -> A e. C)
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 953   e. wcel 955
This theorem is referenced by:  eqeltrrd 1541  syl5eqel 1544  syl6eqel 1548  unisn2 2866  onuninsuc 3098  nlimsucg 3102  dffo3 3804  iunexg 3847  elimdeloprv 3986  1stdm 4093  tz9.12lem3 4633  rankon 4643  rankxplim3 4686  oncardon 4792  oncardid 4793  cardcf 4883  addclpi 4992  mulclpi 4993  addclpq 5030  mulclpq 5032  addclsr 5164  mulclsr 5165  axaddopr 5237  axmulopr 5238  axaddrcl 5244  axmulrcl 5246  mulnzcnopr 5671  lbinfmcl 5996  infmrcl 6016  supxrbnd 6038  nn0addclt 6067  flclt 6174  qdivclt 6212  seqzp1 6480  seq0p1 6483  seqzval2t 6485  ser0cl1 6496  sqclt 6542  reclt 6688  imclt 6689  cjclt 6696  reim0bt 6712  absclt 6768  caure 6864  cauim 6865  ser1absdiflem 6866  facclt 6877  facdivt 6879  bccl2t 6909  permnnt 6911  fsumcllem 6952  climaddlem3 7052  climaddc1 7054  climmullem8 7063  climmulc2 7065  climsub 7066  climsubc2 7067  climcmpc1 7075  climabslem 7084  caucvg3a 7100  caucvg3lem 7102  iserzabslem 7114  cvgcmp2lem 7116  cvgcmp2clem 7118  cvgcmp3c 7122  isumreclt 7145  isumcmpi 7150  infcvglem2 7157  infcvglem3 7158  geolimilem 7170  divccncf 7215  isupivth 7225  dsupivthlem 7226  dfef2 7249  efclt 7254  reefcl 7259  efcj 7278  efaddlem6 7285  efaddlem26 7305  efaddlem27 7306  reeftlclt 7322  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  absef01tllem 7328  eirrlem2 7331  eirrlem3 7332  eirrlem4 7333  eirrlem5 7334  abspef01tlub 7336  absefm1le 7352  eflegeolem2 7354  sinclt 7373  cosclt 7374  resinclt 7380  recosclt 7381  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem1 7433  acdc5lem2 7434  acdclem 7436  iunopnt 7541  tpsex 7547  istps 7548  tgval3t 7567  tgtopt 7570  basgen2t 7581  indistop 7590  iincld 7621  clscld 7625  ntropn 7626  cmclsopn 7635  cmntrcld 7636  idcn 7705  iscncl 7709  cnconst 7719  metres 7763  metxpcl 7772  lmfexlem2 7892  oprcn 7911  opr1cn 7912  opr2cn 7913  fsumcnlem 7923  bcthlem11 7943  bcthlem24 7956  bcthlem25 7957  grpidcl 7993  grpinvcl 8002  grpinvf 8014  issubgi 8059  readdsubg 8066  zaddsubg 8067  ablmul 8068  nvvc 8174  ipcl 8299  ip1cnilem5 8311  nmoxr 8361  siii 8444  minveclem17 8492  minveclem20 8495  minveclem22 8497  minveclem30 8505  minveclem31 8506  htthlem5 8554  spwcl 8583  efif 8636  circgrpOLD 8658  effoi 8666  effoiOLD 8667  hvsubclt 8808  shsubclt 9010  shsubcltOLD 9011  hhssabl 9053  hhssnv 9054  axpjclt 9155  spanclt 9219  hsupclt 9222  sshjclt 9242  spansncht 9399  hosclt 9440  homclt 9441  hodclt 9442  spansnsclt 9510  3oalem2 9525  pjocin 9560  pjoi0t 9579  mayete3 9590  hococl 9608  nmopxrt 9710  nmfnxrt 9723  eigvalclt 9801  lnophmt 9859  bdophm 9877  cnlnadjlem2 9916  cnlnadjlem4 9918  cnlnadjlem5 9919  adjbdlnt 9931  adjbdlnb 9932  branmfnt 9951  brabnt 9952  rnbra 9953  pjcocl 9998  pjcohocl 10041  pj2cocl 10043  spansnat 10185  atord 10219  cdj3lem2a 10268  cdj3lem3a 10271  ghomgrpilem2 10291  idhme 10409  hmphre 10417  qusp 10430  oefil2 10441  neifil 10442  filintf 10443  clicls 10466  mslb1 10473  2wsms 10474  dedalg 10520  aidm 10527  aidmold 10528  catded 10541  isfuna 10592
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465
Copyright terms: Public domain