Theorem eqeltrd 1548

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 1540	. 2 |- (ph -> (A e. C <-> B e. C))
4	1, 3	mpbird 196	1 |- (ph -> A e. C)

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

This theorem is referenced by:  eqeltrrd 1549  syl5eqel 1552  syl6eqel 1556  unisn2 2875  onuninsuc 3108  nlimsucg 3112  dffo3 3819  iunexg 3862  elimdeloprv 4001  1stdm 4109  tz9.12lem3 4661  rankon 4671  rankxplim3 4714  oncardon 4820  oncardid 4821  cardcf 4911  addclpi 5020  mulclpi 5021  addclpq 5058  mulclpq 5060  addclsr 5192  mulclsr 5193  axaddopr 5265  axmulopr 5266  axaddrcl 5272  axmulrcl 5274  mulnzcnopr 5702  lbinfmcl 6049  infmrcl 6069  supxrbnd 6091  nn0addclt 6120  flclt 6226  intfracqOLD 6255  qdivclt 6274  seqzp1 6548  seq0p1 6551  seqzval2t 6553  ser0cl1 6564  sqclt 6611  reclt 6757  imclt 6758  cjclt 6764  reim0bt 6775  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 7486  acdc2lem1 7488  acdc2lem2 7489  acdc5lem1 7491  acdc5lem2 7492  acdclem 7494  iunopnt 7599  tpsex 7605  istps 7606  tgval3t 7625  tgtopt 7628  basgen2t 7639  indistop 7648  iincld 7679  clscld 7683  ntropn 7684  cmclsopn 7693  cmntrcld 7694  idcn 7766  iscncl 7770  cnconst 7780  metres 7823  metxpcl 7832  lmfexlem2 7957  oprcn 7977  opr1cn 7978  opr2cn 7979  fsumcnlem 7989  bcthlem11 8009  bcthlem24 8022  bcthlem25 8023  grpidcl 8059  grpinvcl 8068  grpinvf 8079  issubgi 8122  readdsubg 8129  zaddsubg 8130  ablmul 8131  nvvc 8234  ipcl 8365  ip1cnilem5 8377  nmoxr 8429  siii 8513  minveclem17 8561  minveclem20 8564  minveclem22 8566  minveclem30 8574  minveclem31 8575  htthlem5 8624  spwcl 8660  efif 8721  effoi 8745  hvsubclt 8887  shsubclt 9089  shsubcltOLD 9090  hhssabl 9132  hhssnv 9134  axpjclt 9240  spanclt 9304  hsupclt 9307  sshjclt 9327  spansncht 9483  hosclt 9523  homclt 9524  hodclt 9525  spansnsclt 9593  3oalem2 9608  pjocin 9643  pjoi0t 9662  mayete3 9673  hococl 9691  nmopxrt 9793  nmfnxrt 9806  eigvalclt 9885  lnophmt 9944  bdophm 9962  cnlnadjlem2 10001  cnlnadjlem4 10003  cnlnadjlem5 10004  adjbdlnt 10016  adjbdlnb 10017  branmfnt 10038  brabnt 10039  rnbra 10040  pjcocl 10087  pjcohocl 10131  pj2cocl 10133  spansnat 10277  atord 10311  cdj3lem2a 10363  cdj3lem3a 10366  ghomgrpilem2 10386  idhme 10522  hmphre 10530  qusp 10555  oefil2 10567  neifil 10568  filintf 10569  rcfpfil 10597  rcfpfilOLD 10598  clicls 10622  mslb1 10629  2wsms 10630  dedalg 10676  aidm 10683  aidmold 10684  catded 10697  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain