Theorem eleqtrd 2703

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	|- ( ph -> A e. B )
eleqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eleqtrd	|- ( ph -> A e. C )

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2687	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 222	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eleqtrrd  2704  syl5eleq  2707  syl6eleq  2711  3eltr3d  2715  opth1  4944  0nelop  4960  fviss  6256  tfisi  7058  fnwelem  7292  wfrlem17  7431  omeulem1  7662  oeeulem  7681  oeeui  7682  oaabs2  7725  omabs  7727  ercl  7753  erth  7791  ecelqsdm  7817  ordtypelem6  8428  ordtypelem7  8429  cantnfval  8565  cantnfp1lem3  8577  cantnflem4  8589  r1pwss  8647  rankonidlem  8691  rankxplim3  8744  fseqenlem2  8848  iunfictbso  8937  dfac12lem1  8965  dfac12lem2  8966  fin23lem30  9164  iundom2g  9362  fpwwe2lem6  9457  fpwwe2lem9  9460  lincmb01cmp  12315  fzopth  12378  fzoaddel2  12523  fzosubel2  12527  fzocatel  12531  zpnn0elfzo1  12541  fzoend  12559  peano2fzor  12575  monoord2  12832  sermono  12833  expmulnbnd  12996  bcpasc  13108  swrdcl  13419  revcl  13510  revlen  13511  fsum0diag2  14515  isumsplit  14572  fprodser  14679  sadadd  15189  sadass  15193  smuval2  15204  smumul  15215  vdwapun  15678  vdwlem9  15693  ramub1lem1  15730  prdsbasfn  16131  prdsbasprj  16132  pwsplusgval  16150  pwsmulrval  16151  pwsvscafval  16154  xpsaddlem  16235  xpsvsca  16239  xpsle  16241  mreexmrid  16303  homfeqval  16357  comfval2  16363  comfeq  16366  comfeqval  16368  oppccomfpropd  16387  invco  16431  sectepi  16444  issubc3  16509  funcf2  16528  funciso  16534  fthepi  16588  nat1st2nd  16611  fuciso  16635  homarcl2  16685  coapm  16721  setcmon  16737  setcepi  16738  setcsect  16739  setcinv  16740  setciso  16741  catccatid  16752  resscatc  16755  catciso  16757  catcoppccl  16758  catcfuccl  16759  xpccatid  16828  catcxpccl  16847  xpcpropd  16848  evlfcl  16862  curfpropd  16873  hofcl  16899  yonedalem3  16920  yonffthlem  16922  poslubdg  17149  grpidd  17268  gsumress  17276  ismndd  17313  mndpropd  17316  issubmnd  17318  submnd0  17320  imasmnd  17328  frmdelbas  17390  grpidd2  17459  pwsinvg  17528  imasgrp  17531  submmulg  17586  subginvcl  17603  subgcl  17604  subgsub  17606  subgmulg  17608  quseccl  17650  gaid2  17736  submod  17984  odsubdvds  17986  sylow1lem4  18016  sylow2alem2  18033  lsmdisj2  18095  subgdisj1  18104  pj1id  18112  efgsrel  18147  efgrelexlemb  18163  efgcpbl2  18170  frgpcpbl  18172  frgp0  18173  frgpeccl  18174  frgpadd  18176  frgpup3lem  18190  frgpnabllem1  18276  cycsubgcyg  18302  prdsgsum  18377  dprdfeq0  18421  dmdprdsplitlem  18436  dpjidcl  18457  pgpfac1lem3a  18475  pgpfac1lem4  18477  pgpfaclem1  18480  pgpfaclem2  18481  ablfaclem2  18485  ringidss  18577  ringpropd  18582  imasring  18619  qusring2  18620  kerf1hrm  18743  subrg1  18790  subrgmcl  18792  subrgdv  18797  subrgunit  18798  issubdrg  18805  resrhm  18809  lmodprop2d  18925  0lmhm  19040  lmhmpropd  19073  lspfixed  19128  lssacsex  19144  lbsextlem4  19161  quscrng  19240  assapropd  19327  psrelbas  19379  resspsrvsca  19418  subrgpsr  19419  mplcoe1  19465  mplbas2  19470  mplascl  19496  mplmon2cl  19500  mplmon2mul  19501  evlrhm  19525  mpfconst  19530  vr1cl2  19563  ply1lss  19566  ply1subrg  19567  psropprmul  19608  evl1vsd  19708  evl1expd  19709  evl1gsumadd  19722  evl1gsummon  19729  znf1o  19900  psgnghm2  19927  elocv  20012  pjff  20056  frlmlss  20095  frlmsubgval  20108  frlmvscafval  20109  frlmphl  20120  uvcresum  20132  frlmssuvc1  20133  frlmssuvc2  20134  frlmsslsp  20135  frlmup1  20137  matring  20249  matassa  20250  mat1  20253  mattposcl  20259  mavmulass  20355  mdetunilem9  20426  matinv  20483  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  elcls3  20887  mreclatdemoBAD  20900  neiptopnei  20936  resstps  20991  ordtrest2lem  21007  ordtrest2  21008  pnfnei  21024  mnfnei  21025  iscnp2  21043  iscnp4  21067  cnrest2r  21091  lmcls  21106  lmcld  21107  cnt0  21150  cnhaus  21158  isreg2  21181  connclo  21218  1stccnp  21265  loclly  21290  lly1stc  21299  locfincmp  21329  unisngl  21330  comppfsc  21335  kgencmp2  21349  llycmpkgen2  21353  kgen2ss  21358  kgencn3  21361  pttoponconst  21400  txcls  21407  txbasval  21409  dfac14lem  21420  ptcn  21430  ptrescn  21442  txtube  21443  txcmplem1  21444  txlm  21451  txkgen  21455  xkopjcn  21459  cnmptkp  21483  xkoinjcn  21490  qtopkgen  21513  imastps  21524  isr0  21540  r0cld  21541  pt1hmeo  21609  ptuncnv  21610  ptunhmeo  21611  filintn0  21665  trnei  21696  flimfil  21773  flimopn  21779  fbflim2  21781  cnpflf2  21804  flfcnp  21808  flfcnp2  21811  fclsopn  21818  fcfnei  21839  cnpfcf  21845  flfcntr  21847  alexsublem  21848  ptcmplem3  21858  ptcmplem4  21859  cnextfres1  21872  tmdcn2  21893  tmdgsum  21899  tmdgsum2  21900  symgtgp  21905  tgphaus  21920  tgpt1  21921  qustgplem  21924  prdstmdd  21927  prdstgpd  21928  haustsms  21939  tsmscls  21941  tsmsmhm  21949  tsmsadd  21950  tgptsmscls  21953  tsmssplit  21955  restutop  22041  utopreg  22056  ressusp  22069  ucncn  22089  xmetunirn  22142  ressprdsds  22176  xpsdsval  22186  xblss2ps  22206  blbas  22235  mopntopon  22244  isxms2  22253  imasf1oxms  22294  imasf1oms  22295  prdsxmslem2  22334  tmsxpsval  22343  tngngp2  22456  tngngp  22458  tgioo  22599  metdseq0  22657  cncfmpt2f  22717  cncfcnvcn  22724  cnmptre  22726  cnheibor  22754  nmhmcn  22920  cvsdiv  22932  cvsdivcl  22933  cphsubrglem  22977  cphreccllem  22978  iscmet3  23091  relcmpcmet  23115  bcthlem4  23124  rrxds  23181  minveclem4  23203  ivthicc  23227  evthicc  23228  ovolicc2lem4  23288  ovolicc2lem5  23289  iunmbl2  23325  vitalilem3  23379  cncombf  23425  cnmbf  23426  dvres2lem  23674  cpncn  23699  cpnres  23700  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvcnvlem  23739  dvlip2  23758  dvivth  23773  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  ftc1lem6  23804  mdegvscale  23835  mdegvsca  23836  fta1blem  23928  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  tayl0  24116  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  psercnlem2  24178  psercn  24180  efsubm  24297  cxpcn3  24489  loglesqrt  24499  efrlim  24696  ppinprm  24878  chtnprm  24880  dchrptlem1  24989  dchrptlem2  24990  tgbtwnouttr2  25390  tgldim0eq  25398  tgifscgr  25403  iscgrglt  25409  ercgrg  25412  tgcgrxfr  25413  motcgrg  25439  tglngne  25445  tgcolg  25449  tgbtwnconn1lem2  25468  tgbtwnconn1lem3  25469  legtri3  25485  legbtwn  25489  ncolne1  25520  tgisline  25522  tglinethru  25531  coltr3  25543  colline  25544  tglowdim2ln  25546  mirinv  25561  miriso  25565  mirauto  25579  miduniq  25580  krippenlem  25585  midexlem  25587  ragperp  25612  footex  25613  perpdragALT  25619  perpdrag  25620  colperpexlem1  25622  colperpexlem3  25624  mideulem2  25626  midex  25629  opphllem1  25639  opphllem3  25641  opphllem4  25642  hlpasch  25648  trgcopy  25696  acopyeu  25725  f1otrg  25751  axlowdimlem16  25837  elntg  25864  eengtrkg  25865  eengtrkge  25866  grpoidinv2  27369  grpoinv  27379  ubthlem2  27727  shuni  28159  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  fpwrelmap  29508  gsummpt2d  29781  rngurd  29788  ordtrest2NEWlem  29968  ordtrest2NEW  29969  lmxrge0  29998  nmmulg  30012  rrhcn  30041  esumadd  30119  esumaddf  30123  esumcocn  30142  measiuns  30280  mbfmco2  30327  dya2iocnrect  30343  omscl  30357  omsf  30358  oms0  30359  sibf0  30396  sibfof  30402  sitgaddlemb  30410  fibp1  30463  ccatmulgnn0dir  30619  cxpcncf1  30673  ftc2re  30676  fsum2dsub  30685  reprf  30690  reprsum  30691  bnj1450  31118  bnj1501  31135  indispconn  31216  connpconn  31217  pconnpi1  31219  sconnpi1  31221  cvmsss2  31256  cvmliftmolem1  31263  cvmliftlem8  31274  cvmliftlem10  31276  cvmliftlem11  31277  cvmlift2lem9  31293  cvmlift2lem12  31296  cvmlift3lem7  31307  mrsubcv  31407  mrsubff  31409  mrsubccat  31415  elmrsubrn  31417  mrsubco  31418  mrsubvrs  31419  nodenselem5  31838  linethru  32260  ivthALT  32330  neibastop2  32356  filnetlem4  32376  matunitlindflem2  33406  poimirlem1  33410  poimirlem2  33411  poimirlem8  33417  poimirlem9  33418  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimir  33442  broucube  33443  areacirclem4  33503  fdc  33541  isbnd3  33583  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  rrnequiv  33634  reheibor  33638  iscringd  33797  isfldidl  33867  eqlkr  34386  ldualvsubval  34444  dvalveclem  36314  dia2dimlem5  36357  dia2dimlem9  36361  tendoinvcl  36393  dvhgrp  36396  dvhlveclem  36397  dihpN  36625  dochsnkr2cl  36763  lcfl7lem  36788  lclkr  36822  lclkrs  36828  lcfrvalsnN  36830  lcfrlem4  36834  lcfrlem6  36836  lcfrlem16  36847  lcdvsubval  36907  lcdlkreqN  36911  mapdcl2  36945  mapdincl  36950  mapdlsmcl  36952  mapdpglem3  36964  hdmaprnlem9N  37149  hdmaplkr  37205  hdmapip0  37207  hdmapglem7a  37219  diophin  37336  acongeq  37550  isnumbasgrplem2  37674  proot1mul  37777  iunrelexpuztr  38011  ntrclsiex  38351  ntrneiiex  38374  ntrneinex  38375  bccbc  38544  suctrALT  39061  restuni3  39301  disjf1o  39378  disjinfi  39380  choicefi  39392  fsneq  39398  fsneqrn  39403  unirnmapsn  39406  iunmapsn  39409  fvelimad  39458  monoords  39511  elfzolem1  39537  uzfissfz  39542  evthiccabs  39718  iooabslt  39721  tgqioo2  39774  islptre  39851  limciccioolb  39853  sumnnodd  39862  limcicciooub  39869  lptre2pt  39872  limcresiooub  39874  limcresioolb  39875  lptioo1cn  39878  reclimc  39885  liminfvalxr  40015  liminfvaluz  40024  limsupvaluz3  40030  fsumcncf  40091  ioccncflimc  40098  cncfuni  40099  icccncfext  40100  cncficcgt0  40101  icocncflimc  40102  cncfdmsn  40103  cncfiooicclem1  40106  cncfiooicc  40107  cncfioobd  40110  cxpcncf2  40113  fprodsub2cncf  40119  fprodadd2cncf  40120  fperdvper  40133  dvcosax  40141  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  itgsubsticclem  40191  fvvolioof  40206  fvvolicof  40208  stoweidlem26  40243  stoweidlem27  40244  stoweidlem31  40248  stoweidlem34  40251  dirkercncflem2  40321  dirkercncflem3  40322  dirkercncflem4  40323  dirkercncf  40324  fourierdlem16  40340  fourierdlem20  40344  fourierdlem21  40345  fourierdlem22  40346  fourierdlem26  40350  fourierdlem32  40356  fourierdlem33  40357  fourierdlem38  40362  fourierdlem39  40363  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem53  40376  fourierdlem60  40383  fourierdlem61  40384  fourierdlem69  40392  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem100  40423  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriersw  40448  fouriercn  40449  etransclem24  40475  etransclem26  40477  etransclem28  40479  etransclem31  40482  etransclem32  40483  etransclem33  40484  etransclem34  40485  etransclem35  40486  etransclem38  40489  rrxbasefi  40503  rrxdsfi  40505  rrxtopnfi  40506  rrxmetfi  40507  rrxtoponfi  40511  qndenserrnbl  40515  qndenserrnopnlem  40517  qndenserrn  40519  rrnprjdstle  40521  ioorrnopnlem  40524  prsal  40538  intsaluni  40547  salgencntex  40561  subsaliuncllem  40575  fge0iccico  40587  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0pr  40611  sge0isum  40644  nnfoctbdjlem  40672  iundjiunlem  40676  iundjiun  40677  meadjiunlem  40682  psmeasure  40688  meaiininclem  40700  caragenelss  40715  omeunile  40719  carageniuncllem1  40735  carageniuncllem2  40736  0ome  40743  isomenndlem  40744  isomennd  40745  hoicvr  40762  ovnpnfelsup  40773  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvle  40814  ovnhoilem1  40815  hoi2toco  40821  ovncvr2  40825  hspdifhsp  40830  voncmpl  40835  hoiqssbl  40839  hspmbllem2  40841  hspmbl  40843  hoimbllem  40844  opnvonmbllem2  40847  mblvon  40853  ovolval3  40861  ovolval4lem1  40863  ovnovollem1  40870  ovnovollem2  40871  vonsn  40905  issmflem  40936  sssmf  40947  issmflelem  40953  issmfgtlem  40964  issmfgt  40965  smfaddlem1  40971  issmfgelem  40977  smflimlem3  40981  smfmullem2  40999  smfmullem4  41001  smfsuplem1  41017  smfsupmpt  41021  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem4  41029  smflimsupmpt  41035  smfliminfmpt  41038  fzoopth  41337  issubmgm2  41790  zlmodzxzel  42133  ply1mulgsum  42178