Theorem eqeltrd 1551

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

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 |- (ph -> B e. C)
2		eqeltrd.1	. . 3 |- (ph -> A = B)
3	2	eleq1d 1543	. 2 |- (ph -> (A e. C <-> B e. C))
4	1, 3	mpbird 196	1 |- (ph -> A e. C)

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960

This theorem is referenced by:  eqeltrrd 1552  syl5eqel 1555  syl6eqel 1559  unisn2 2881  onuninsuc 3114  nlimsucg 3118  dffo3 3825  iunexg 3868  elimdeloprv 4007  1stdm 4115  tz9.12lem3 4671  rankon 4681  rankxplim3 4724  oncardon 4830  oncardid 4831  cardcf 4923  addclpi 5032  mulclpi 5033  addclpq 5070  mulclpq 5072  addclsr 5204  mulclsr 5205  axaddopr 5277  axmulopr 5278  axaddrcl 5284  axmulrcl 5286  mulnzcnopr 5714  lbinfmcl 6051  infmrcl 6071  supxrbnd 6093  nn0addclt 6122  flclt 6228  intfracq 6255  qdivclt 6275  seqzp1 6549  seq0p1 6552  seqzval2t 6554  ser0cl1 6565  sqclt 6612  reclt 6758  imclt 6759  cjclt 6765  reim0bt 6776  absclt 6833  caure 6927  cauim 6928  ser1absdiflem 6929  facclt 6940  facdivt 6942  bccl2t 6971  permnnt 6973  fsumcllem 7014  climaddlem3 7116  climaddc1 7118  climmullem8 7127  climmulc2 7129  climsub 7130  climsubc2 7131  climcmpc1 7139  climabslem 7148  caucvg3a 7164  caucvg3lem 7166  iserzabslem 7178  cvgcmp2lem 7180  cvgcmp2clem 7182  cvgcmp3c 7186  isumreclt 7210  isumcmpi 7215  infcvglem2 7222  infcvglem3 7223  geolimilem 7235  divccncf 7280  isupivth 7290  dsupivthlem 7291  dfef2 7307  efclt 7312  reefcl 7317  efcj 7336  efaddlem6 7343  efaddlem26 7363  efaddlem27 7364  reeftlclt 7380  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem2 7390  eirrlem3 7391  eirrlem4 7392  eirrlem5 7393  abspef01tlub 7395  absefm1le 7412  eflegeolem2 7414  sinclt 7431  cosclt 7432  resinclt 7438  recosclt 7439  acdc3lem 7487  acdc2lem1 7489  acdc2lem2 7490  acdc5lem1 7492  acdc5lem2 7493  acdclem 7495  iunopnt 7600  tpsex 7606  istps 7607  tgval3t 7624  tgtopt 7627  basgen2t 7638  indistop 7645  iincld 7676  clscld 7680  ntropn 7681  cmclsopn 7690  cmntrcld 7691  idcn 7763  iscncl 7767  cnconst 7777  metres 7820  metxpcl 7829  lmfexlem2 7954  oprcn 7974  opr1cn 7975  opr2cn 7976  fsumcnlem 7986  bcthlem11 8006  bcthlem24 8019  bcthlem25 8020  grpidcl 8055  grpinvcl 8064  grpinvf 8075  issubgi 8118  readdsubg 8125  zaddsubg 8126  ablmul 8127  nvvc 8230  ipcl 8361  ip1cnilem5 8373  nmoxr 8425  siii 8509  minveclem17 8557  minveclem20 8560  minveclem22 8562  minveclem30 8570  minveclem31 8571  htthlem5 8620  spwcl 8656  efif 8716  effoi 8740  hvsubclt 8882  shsubclt 9084  shsubcltOLD 9085  hhssabl 9127  hhssnv 9129  axpjclt 9235  spanclt 9299  hsupclt 9302  sshjclt 9322  spansncht 9478  hosclt 9518  homclt 9519  hodclt 9520  spansnsclt 9588  3oalem2 9603  pjocin 9638  pjoi0t 9657  mayete3 9668  hococl 9686  nmopxrt 9788  nmfnxrt 9801  eigvalclt 9880  lnophmt 9939  bdophm 9957  cnlnadjlem2 9996  cnlnadjlem4 9998  cnlnadjlem5 9999  adjbdlnt 10011  adjbdlnb 10012  branmfnt 10033  brabnt 10034  rnbra 10035  pjcocl 10082  pjcohocl 10126  pj2cocl 10128  spansnat 10272  atord 10306  cdj3lem2a 10358  cdj3lem3a 10361  ghomgrpilem2 10381  idhme 10508  hmphre 10516  qusp 10541  oefil2 10552  neifil 10553  filintf 10554  rcfpfil 10569  clicls 10593  mslb1 10600  2wsms 10601  dedalg 10647  aidm 10654  catded 10668  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475

Copyright terms: Public domain