Theorem eqeltrd 2216

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eqeltrrd  2217  3eltr4d  2223  eqeltrid  2226  eqeltrdi  2230  ifcldadc  3501  ifcldcd  3507  intab  3800  disjiun  3924  iinexgm  4079  opexg  4150  tfisi  4501  nnpredcl  4536  imain  5205  fvmptd  5502  fvmptdf  5508  fvmptt  5512  elfvmptrab  5516  dffo3  5567  resfunexg  5641  f1oiso2  5728  riota2df  5750  riota5f  5754  ovmpodxf  5896  ovmpodf  5902  offval  5989  ofvalg  5991  offeq  5995  iunexg  6017  oprabexd  6025  fo1stresm  6059  fo2ndresm  6060  oprssdmm  6069  1stdm  6080  1stconst  6118  2ndconst  6119  cnvf1olem  6121  fo2ndf  6124  f1od2  6132  iunon  6181  tfrlemibacc  6223  tfrlemibfn  6225  tfr1onlembacc  6239  tfr1onlembfn  6241  tfrcllembacc  6252  tfrcllembfn  6254  tfrcl  6261  rdgon  6283  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  oacl  6356  omcl  6357  oeicl  6358  nntr2  6399  mptelixpg  6628  fidifsnen  6764  en2eqpr  6801  unfiin  6814  ssfirab  6822  fnfi  6825  relcnvfi  6829  fidcenumlemr  6843  elfi2  6860  supclti  6885  supubti  6886  suplubti  6887  supelti  6889  ordiso2  6920  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djuss  6955  updjudhcoinlf  6965  updjudhcoinrg  6966  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  cardcl  7037  addclpi  7135  mulclpi  7136  addclnq  7183  mulclnq  7184  addclnq0  7259  mulclnq0  7260  nqpnq0nq  7261  elnp1st2nd  7284  prarloclemcalc  7310  distrlem1prl  7390  distrlem1pru  7391  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  addcanprlemu  7423  recexprlemloc  7439  aptiprleml  7447  caucvgprprlemopl  7505  suplocexprlemex  7530  addclsr  7561  mulclsr  7562  recexgt0sr  7581  mulextsr1lem  7588  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axaddcl  7672  axaddrcl  7673  axmulcl  7674  axmulrcl  7675  axcaucvglemval  7705  subcl  7961  cru  8364  aprcl  8408  divclap  8438  redivclap  8491  diveqap1bd  8595  lbinfcl  8707  cju  8719  nn1m1nn  8738  nnsub  8759  nnnn0addcl  9007  un0addcl  9010  peano2z  9090  peano2zm  9092  zaddcllemneg  9093  zaddcl  9094  nnaddm1cl  9115  nn0n0n1ge2  9121  zdivadd  9140  zdivmul  9141  suprzclex  9149  zneo  9152  peano5uzti  9159  supinfneg  9390  infsupneg  9391  qmulz  9415  qnegcl  9428  qapne  9431  qdivcl  9435  cnref1o  9440  xnegcl  9615  xltnegi  9618  xaddnemnf  9640  xaddnepnf  9641  xnegdi  9651  xnpcan  9655  xltadd1  9659  xposdif  9665  xleaddadd  9670  iccf1o  9787  ige3m2fz  9829  ige2m1fz1  9889  rebtwn2z  10032  flqcl  10046  flapcl  10048  ceilqcl  10081  intfracq  10093  modqcl  10099  mulqmod0  10103  modqdifz  10109  zmodcl  10117  modfzo0difsn  10168  modsumfzodifsn  10169  frec2uzzd  10173  frec2uzsucd  10174  frec2uzuzd  10175  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  fzofig  10205  iseqovex  10229  seq3val  10231  seqvalcd  10232  seqf  10234  seqovcd  10236  seq3clss  10240  seq3caopr3  10254  iseqf1olemnab  10261  iseqf1olemqk  10267  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsum  10273  seq3f1oleml  10276  seq3f1o  10277  seq3distr  10286  ser0f  10288  ser3le  10291  exp3vallem  10294  exp3val  10295  exp1  10299  expcl2lemap  10305  m1expcl2  10315  expaddzap  10337  sqcl  10354  nnsqcl  10362  qsqcl  10364  zesq  10410  facp1  10476  faccl  10481  facdiv  10484  bcval  10495  bcrpcl  10499  bcp1n  10507  bcpasc  10512  permnn  10517  hashennn  10526  hashcl  10527  shftlem  10588  ovshftex  10591  shftf  10602  seq3shft  10610  cjth  10618  imval  10622  recl  10625  imcl  10626  crre  10629  remim  10632  reim0b  10634  cvg1nlemcau  10756  uzin2  10759  resqrexlem1arp  10777  resqrexlemp1rp  10778  resqrexlemglsq  10794  resqrexlemga  10795  resqrtcl  10801  abscl  10823  absrpclap  10833  nn0abscl  10857  fzomaxdiflem  10884  fzomaxdif  10885  maxabslemab  10978  maxcl  10982  zmaxcl  10996  minmax  11001  mincl  11002  xrmaxcl  11021  xrmaxaddlem  11029  xrminmax  11034  xrmincl  11035  xrmineqinf  11038  xrminrpcl  11043  reccn2ap  11082  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  climle  11103  climlec2  11110  climcvg1nlem  11118  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  zsumdc  11153  fsumgcl  11155  fsum3  11156  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsum3ser  11166  fsumcl2lem  11167  fsumcllem  11168  fsumadd  11175  sumsnf  11178  fsumsplitsn  11179  isumcl  11194  isummulc2  11195  isumrecl  11198  isumge0  11199  isumadd  11200  fsum2dlemstep  11203  fisumcom2  11207  mptfzshft  11211  fsumrev  11212  fsummulc2  11217  iserabs  11244  isumshft  11259  isumsplit  11260  isum1p  11261  isumrpcl  11263  isumle  11264  isumlessdc  11265  trireciplem  11269  expcnvap0  11271  expcnvre  11272  expcnv  11273  explecnv  11274  geolim  11280  geolim2  11281  geo2lim  11285  cvgratnnlemsumlt  11297  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodf1f  11312  prodfdivap  11316  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  efcllemp  11364  ef0lem  11366  efcvgfsum  11373  reefcl  11374  ege2le3  11377  efcj  11379  efaddlem  11380  eftlcvg  11393  eftlcl  11394  reeftlcl  11395  eftlub  11396  efsep  11397  effsumlt  11398  efgt1p2  11401  efgt1p  11402  reeff1  11407  tanclap  11416  resincl  11427  recoscl  11428  retanclap  11429  eirraplem  11483  dvdsval2  11496  sqoddm1div8z  11583  zssinfcl  11641  infssuzex  11642  infssuzcldc  11644  gcdval  11648  gcdn0cl  11651  gcddvds  11652  divgcdnnr  11664  nn0seqcvgd  11722  ialgrlem1st  11723  ialgrlemconst  11724  algrf  11726  algrp1  11727  eucalgf  11736  eucalglt  11738  lcmval  11744  lcmcllem  11748  lcmgcdlem  11758  cncongr2  11785  sqrt2irrlem  11839  oddpwdclemxy  11847  oddpwdclemdc  11851  qden1elz  11883  phicl2  11890  phimullem  11901  ennnfonelemjn  11915  ennnfonelemg  11916  ennnfonelemp1  11919  ctinfomlemom  11940  ctiunctlemfo  11952  setsex  11991  strsetsid  11992  ressid2  12018  ressval2  12019  ressid  12020  iunopn  12169  toponmax  12192  tgvalex  12219  tgtop  12237  tgiun  12242  tgidm  12243  ntropn  12286  tgrest  12338  restopnb  12350  cnovex  12365  cnclima  12392  txvalex  12423  txtop  12429  tx1cn  12438  tx2cn  12439  txcnp  12440  txcnmpt  12442  txdis1cn  12447  cnmptcom  12467  imasnopn  12468  hmeocnv  12476  hmeores  12484  txhmeo  12488  txswaphmeo  12490  ispsmet  12492  xmetres  12551  metres  12552  blex  12556  xmeter  12605  xmetresbl  12609  mopntopon  12612  isxms2  12621  xmetxp  12676  xmettx  12679  txmetcnp  12687  qtopbasss  12690  qtopbas  12691  reopnap  12707  ioo2blex  12713  blssioo  12714  tgioo  12715  fsumcncntop  12725  cncfval  12728  divccncfap  12746  cdivcncfap  12756  ivthdec  12791  limccnpcntop  12813  dvrecap  12846  pilem3  12864  tanrpcl  12918  cosordlem  12930  djucllem  13007  nninfsellemeq  13210  qdencn  13222  isomninnlem  13225  cvgcmp2nlemabs  13227  trilpolemclim  13229  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234