MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltrrd Structured version   Unicode version

Theorem eqeltrrd 2540
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eqeltrrd.1  |-  ( ph  ->  A  =  B )
eqeltrrd.2  |-  ( ph  ->  A  e.  C )
Assertion
Ref Expression
eqeltrrd  |-  ( ph  ->  B  e.  C )

Proof of Theorem eqeltrrd
StepHypRef Expression
1 eqeltrrd.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2459 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2539 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446
This theorem is referenced by:  3eltr3d  2553  tz7.7  4843  fvmptdv2  5886  ffvresb  5973  xpexr2  6619  2ndrn  6722  1st2ndbr  6723  elopabi  6735  cnvf1olem  6770  dftpos4  6864  seqomlem4  7008  oneo  7120  oeordi  7126  oeeulem  7140  oeeui  7141  nnmordi  7170  nnneo  7190  th3qlem1  7306  disjen  7568  fnfi  7690  fsuppco  7752  elfi2  7765  fisupcl  7818  ordiso2  7830  ordtypelem9  7841  hartogslem2  7858  unxpwdom2  7904  noinfep  7966  cantnflt  7981  cantnfp1lem3  7989  cantnflem1  7998  cantnflem3  8000  cantnf  8002  cantnfltOLD  8011  cantnfp1lem3OLD  8015  cantnflem1OLD  8021  cantnflem3OLD  8022  cantnfOLD  8024  cnfcom3lem  8037  cnfcom3lemOLD  8045  r1pwss  8092  r0weon  8280  alephfp  8379  dfac2a  8400  cfsmolem  8540  enfin2i  8591  ac6num  8749  ttukeylem7  8785  fpwwe2lem9  8906  canthp1lem2  8921  pwfseqlem4  8930  gchaleph2  8940  wunun  8978  r1tskina  9050  tskun  9054  gruen  9080  subf  9713  resubcl  9774  negcon1ad  9815  subeq0bd  9875  rimul  10414  peano2nn  10435  nn0nnaddcl  10712  elnn0nn  10723  elz2  10764  zsubcl  10788  zrevaddcl  10791  zdiv  10813  peano5uzi  10831  peano2uzr  11011  uzaddcl  11012  qsubcl  11073  qrevaddcl  11076  xov1plusxeqvd  11532  fseq1p1m1  11635  om2uzrani  11876  uzrdglem  11881  seqf1olem2  11947  expaddzlem  12008  expaddz  12009  expmulz  12011  zesq  12088  bcm1k  12192  bccl  12199  permnn  12203  hashcl  12227  hashf1lem2  12311  hashf1  12312  seqcoll  12318  shftuz  12660  ref  12703  imf  12704  crre  12705  rereb  12711  absf  12927  lo1res2  13142  o1res2  13143  o1add2  13203  o1mul2  13204  o1sub2  13205  lo1sub  13210  isercoll2  13248  summolem2a  13294  fsumf1o  13302  fsumcnv  13342  mptfzshft  13347  geolim2  13433  ruclem12  13625  sqr2irrlem  13632  oexpneg  13697  3dvds  13698  bitsf1  13744  gcdf  13805  sqnprm  13886  fnum  13922  fden  13923  phimullem  13956  pc2dvds  14047  gzsubcl  14103  4sqlem5  14105  4sqlem9  14109  4sqlem10  14110  mul4sqlem  14116  mul4sq  14117  4sqlem11  14118  4sqlem13  14120  4sqlem16  14123  4sqlem17  14124  4sqlem18  14125  vdwlem5  14148  vdwlem8  14151  vdwlem9  14152  ramub1lem2  14190  firest  14473  prdsplusg  14498  prdsmulr  14499  prdsvsca  14500  prdshom  14507  prdsbascl  14523  xpsaddlem  14615  xpsvsca  14619  xpsle  14621  mreincl  14639  ismred2  14643  mrcidb  14655  ssclem  14834  idffth  14945  ressffth  14950  coapm  15041  catciso  15077  evlfcl  15134  diag2cl  15158  hofcllem  15170  hofcl  15171  yonffthlem  15194  yoniso  15197  subsubm  15587  mhmima  15593  frmdss2  15643  mulgdir  15754  imasgrp2  15772  subgmulg  15797  issubg2  15798  issubgrpd2  15799  grpissubg  15803  subsubg  15806  cycsubgcl  15809  isnsg3  15817  ssnmz  15825  eqger  15833  ghmrn  15862  ghmnsgima  15872  conjsubg  15880  conjnmz  15882  subggim  15896  gass  15921  symggen  16078  psgnunilem1  16101  psgnunilem3  16104  mndodconglem  16148  odsubdvds  16174  sylow1lem1  16201  sylow1lem3  16203  sylow1lem4  16204  pgpssslw  16217  sylow2a  16222  sylow2blem3  16225  slwhash  16227  fislw  16228  sylow3lem2  16231  sylow3lem4  16233  sylow3lem5  16234  sylow3lem6  16235  lsmub1x  16249  lsmub2x  16250  lsmsubm  16256  lsmmod  16276  lsmdisj2  16283  subgdisj1  16292  efginvrel2  16328  efgsres  16339  efgsfo  16340  efgredleme  16344  iscygodd  16469  prmcyg  16474  gsumzsubmclOLD  16507  gsummptfsaddOLD  16519  gsum2d2lem  16570  pwsgsumOLD  16579  dprdcntz  16597  dprddisj  16598  dprdw  16599  dprdwOLD  16605  dprdfeq0  16617  dprdf11  16618  dprdfidOLD  16619  dprdfinvOLD  16621  dprdfaddOLD  16622  dprdfsubOLD  16623  dprdfeq0OLD  16624  dprdf11OLD  16625  dprdsubg  16626  dprdub  16627  dprdres  16630  dprdf1o  16634  dmdprdsplitlemOLD  16640  dprddisj2OLD  16643  dprd2dlem2  16644  dprd2dlem1  16645  dprd2da  16646  dmdprdsplit2  16650  dpjfval  16659  dpjidclOLD  16669  ablfacrplem  16671  ablfacrp  16672  ablfac1c  16677  ablfac1eu  16679  pgpfac1lem3a  16682  pgpfac1lem3  16683  pgpfaclem1  16687  pgpfaclem3  16689  ablfaclem3  16693  0unit  16878  irredneg  16908  irrednegb  16909  isdrng2  16948  subrgcrng  16975  subrgin  16994  subsubrg  16997  srngcl  17046  islmodd  17060  lssvancl1  17132  lss0cl  17134  lssvacl  17141  lssvscl  17142  lssvnegcl  17143  lssincl  17152  lmhmima  17234  lmhmrnlss  17237  lsslvec  17294  lspabs3  17308  lspdisj  17312  lspexch  17316  lsmcv  17328  lspsolv  17330  issubrngd2  17376  rlmlvec  17393  lidl1el  17406  drngnidl  17417  2idlcpbl  17422  isassad  17500  issubassa2  17521  psrass1lem  17553  mvridlemOLD  17599  mplsubrglem  17624  mplsubrglemOLD  17625  mplmonmul  17650  mplcoe3OLD  17653  mplcoe5  17655  mplcoe2OLD  17657  subrgasclcl  17688  mplmon2cl  17689  mplind  17691  evlsval2  17713  mpfconst  17723  mpfproj  17724  mpfaddcl  17727  mpfmulcl  17728  pf1const  17889  pf1id  17890  pf1subrg  17891  mpfpf1  17894  pf1addcl  17896  pf1mulcl  17897  pf1ind  17898  zsssubrg  17980  cnsubrg  17982  gzrngunit  17987  zringlpirlem1  18012  zlpirlem1  18017  frgpcyg  18115  zrhpsgninv  18124  isphld  18192  css0  18223  pjfo  18249  frlmgsumOLD  18304  frlmsplit2  18306  frlmphllem  18314  frlmphl  18315  uvcresum  18327  mdetunilem6  18539  unopn  18632  istps2OLD  18642  tsettps  18664  tgss2  18708  difopn  18754  incld  18763  iuncld  18765  indiscld  18811  mretopd  18812  resttop  18880  resttopon  18881  restfpw  18899  ordtbaslem  18908  ordtbas2  18911  ordtbas  18912  ordttopon  18913  ordtopn1  18914  ordtopn2  18915  ordtcld1  18917  ordtcld2  18918  ordtrest  18922  ordtrest2  18924  tgcn  18972  tgcnp  18973  cnpco  18987  cnt1  19070  cnrmnrm  19081  conndisj  19136  uncon  19149  2ndctop  19167  2ndcrest  19174  2ndcctbss  19175  2ndcomap  19178  dis2ndc  19180  restnlly  19202  islly2  19204  llyidm  19208  nllyidm  19209  dislly  19217  kgeni  19226  kgencmp2  19235  iskgen2  19237  kgencn2  19246  kgencn3  19247  elptr2  19263  ptbasfi  19270  txcld  19292  xkoccn  19308  txcn  19315  txdis  19321  txkgen  19341  xkopjcn  19345  xkococnlem  19348  cnmpt11  19352  cnmpt11f  19353  cnmpt1t  19354  cnmpt12  19356  cnmpt21  19360  cnmpt21f  19361  cnmpt2t  19362  cnmpt22  19363  cnmpt22f  19364  cnmpt1res  19365  cnmptkp  19369  cnmptk1  19370  cnmpt1k  19371  cnmptkk  19372  cnmptk1p  19374  cnmptk2  19375  cnmpt2k  19377  txcon  19378  basqtop  19400  tgqtop  19401  qtopeu  19405  qtoprest  19406  qtopomap  19407  qtopcmap  19408  r0cld  19427  ordthmeolem  19490  pt1hmeo  19495  ptcmpfi  19502  xkocnv  19503  xkohmeo  19504  fbdmn0  19523  trfil1  19575  trfil2  19576  trfg  19580  uzrest  19586  uzfbas  19587  trufil  19599  elfm3  19639  rnelfm  19642  fmfnfmlem2  19644  fmfnfm  19647  txflf  19695  alexsublem  19732  alexsub  19733  alexsubb  19734  ptcmplem3  19742  ptcmplem4  19743  cnmpt1plusg  19774  cnmpt2plusg  19775  istgp2  19778  oppgtgp  19785  symgtgp  19788  subgtgp  19792  subgntr  19793  opnsubg  19794  cldsubg  19797  tgpconcomp  19799  tgpt0  19805  divstgplem  19807  divstgphaus  19809  prdstmdd  19810  tsms0  19831  tsmsadd  19837  tsmsxplem1  19843  tsmsxplem2  19844  cnmpt1vsca  19884  cnmpt2vsca  19885  trust  19920  uspreg  19965  xpsdsval  20072  xmeter  20124  mscl  20152  xmscl  20153  blcld  20196  stdbdxmet  20206  met2ndci  20213  prdsxmslem2  20220  tmsxps  20227  metustidOLD  20250  metustid  20251  tngngpd  20355  tngnrg  20371  sranlm  20381  lssnlm  20397  lssnvc  20398  xrsxmet  20502  xrsblre  20504  zdis  20509  icccmplem2  20516  xrge0tsms  20527  cnmpt1ds  20535  cnmpt2ds  20536  cncfmpt1f  20605  negcncf  20610  negfcncf  20611  cnheiborlem  20642  evth  20647  evth2  20648  lebnumlem1  20649  lebnumlem3  20651  xlebnum  20653  copco  20706  pcopt  20710  pcopt2  20711  pi1addf  20735  pi1addval  20736  pi1cof  20747  pi1coghm  20749  isclmi  20765  cphsubrglem  20812  cphreccllem  20813  cphcjcl  20818  cphsqrcl2  20821  cphsqrcl3  20822  cphqss  20823  cphnmf  20830  reipcl  20832  ipcau2  20865  cnmpt1ip  20875  cnmpt2ip  20876  clsocv  20878  iscauf  20907  cmetcaulem  20915  lmle  20928  lmcau  20939  lssbn  20978  hlprlem  20995  ishl2  20998  minveclem3b  21031  pjthlem2  21041  ovolfcl  21066  ovoliunlem1  21101  ovolshftlem1  21108  ovolicc2lem3  21118  ovolicc2lem4  21119  shftmbl  21136  inmbl  21139  difmbl  21140  volinun  21143  volfiniun  21144  voliunlem3  21149  volsup  21153  icombl1  21160  icombl  21161  ioombl  21162  iccmbl  21163  uniioombllem3  21181  uniioombllem5  21183  uniiccmbl  21186  dyaddisjlem  21191  dyadmbl  21196  opnmbllem  21197  volcn  21202  vitalilem1  21204  vitalilem4  21207  mbfdm  21222  mbfimasn  21228  mbfdm2  21232  mbfmulc2lem  21241  mbfmulc2re  21242  mbfneg  21244  mbfpos  21245  mbfposr  21246  mbfposb  21247  ismbf3d  21248  mbfimaopnlem  21249  cncombf  21252  mbfaddlem  21254  mbfadd  21255  mbfsub  21256  mbfmulc2  21257  mbflimsup  21260  mbflimlem  21261  i1fima  21272  i1fima2  21273  i1fima2sn  21274  i1fd  21275  i1f0rn  21276  itg11  21285  i1faddlem  21287  i1fadd  21289  i1fmul  21290  itg1addlem2  21291  itg1addlem4  21293  itg1addlem5  21294  itg1mulc  21298  i1fres  21299  i1fposd  21301  i1fsub  21302  itg1climres  21308  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1flimlem  21316  mbfi1flim  21317  mbfmullem2  21318  mbfmul  21320  itg2const  21334  itg2const2  21335  itg2seq  21336  itg2splitlem  21342  itg2monolem1  21344  itg2mono  21347  itg2gt0  21354  itg2cnlem1  21355  iblss  21398  i1fibl  21401  itgitg1  21402  itgss3  21408  ibladd  21414  iblsub  21415  iblabs  21422  bddmulibl  21432  bddibl  21433  cnmptlimc  21481  limccnp  21482  limccnp2  21483  perfdvf  21494  dvcnp2  21510  cpnord  21525  cpncn  21526  cpnres  21527  dvcnvlem  21564  cmvth  21579  dvlip  21581  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  c1lip1  21585  c1lip2  21586  dvgt0lem1  21590  lhop1lem  21601  lhop2  21603  lhop  21604  dvcnvrelem2  21606  dvcnvre  21607  dvfsumle  21609  dvfsumabs  21611  dvfsumlem2  21615  ftc1lem1  21623  ftc1lem2  21624  ftc1a  21625  ftc1lem4  21627  ftc2  21632  ftc2ditglem  21633  ftc2ditg  21634  itgsubstlem  21636  deg1pwle  21707  deg1submon1p  21740  plyco0  21776  elplyd  21786  plypow  21789  plyconst  21790  plypf1  21796  plysub  21803  dgrcolem1  21856  dgrcolem2  21857  vieta1lem1  21892  vieta1lem2  21893  iaa  21907  aalioulem1  21914  aalioulem4  21917  aaliou3lem6  21930  tayl0  21943  taylpfval  21946  taylthlem2  21955  ulmdvlem1  21981  ulmdvlem3  21983  mtest  21985  mtestbdd  21986  mbfulm  21987  iblulm  21988  itgulm  21989  psercn2  22004  psercn  22007  abelthlem1  22012  abelthlem3  22014  abelth  22022  abelth2  22023  sincn  22025  coscn  22026  efcvx  22030  pige3  22095  cosne0  22102  tanregt0  22111  efif1olem4  22117  relogcl  22143  logdiv2  22182  logcn  22208  dvloglem  22209  logf1o2  22211  efopnlem2  22218  logccv  22224  cxpsqr  22264  loglesqr  22312  ang180lem1  22321  ang180lem2  22322  isosctrlem2  22333  angpined  22341  mcubic  22358  atanbnd  22437  atans2  22442  atantayl2  22449  atantayl3  22450  leibpi  22453  rlimcnp2  22476  efrlim  22479  cvxcl  22494  emcllem6  22510  fsumharmonic  22521  ftalem2  22527  ftalem7  22532  basellem2  22535  basellem3  22536  basellem5  22538  basellem9  22542  ppiprm  22605  ppinprm  22606  chtprm  22607  chtnprm  22608  efchtdvds  22613  fsumdvdsmul  22651  chtublem  22666  fsumvma  22668  mersenne  22682  perfect  22686  dchrfi  22710  lgsne0  22788  lgseisenlem4  22807  lgsquadlem1  22809  2sqblem  22832  chebbnd2  22842  chto1lb  22843  rpvmasumlem  22852  dchrisumlem2  22855  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0re  22878  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrmusumlem  22887  dchrvmasumlem  22888  rpvmasum  22891  rplogsum  22892  mudivsum  22895  mulog2sumlem3  22901  2vmadivsumlem  22905  selberglem2  22911  selberg2lem  22915  logdivbnd  22921  selberg3lem1  22922  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntpbnd2  22952  pntlemo  22972  tgbtwnexch2  23067  tgbtwnxfr  23098  tghilbert1_1  23165  coltr3  23176  colline  23177  mirreu3  23184  colperplem1  23240  ttgcontlem1  23266  iseupa  23721  ablomul  23977  ghgrp  23990  rngoablo2  24044  vcoprne  24092  nvi  24127  ipval2lem3  24235  ipval2lem6  24241  ipf  24246  ubthlem1  24406  minvecolem2  24411  minvecolem4a  24413  hhshsslem2  24804  shsel1  24859  pjoccl  24971  5oalem1  25192  5oalem5  25196  3oalem2  25201  pjrni  25240  hmopd  25561  imaelshi  25597  adjbdlnb  25623  adjsslnop  25626  bracnlnval  25653  hmopidmchi  25690  disjabrex  26060  disjabrexf  26061  fgreu  26124  ffsrn  26163  fpwrelmapffslem  26166  archiabllem2c  26346  xrge0tsmsd  26387  suborng  26417  metideq  26454  ordtrestNEW  26485  ordtrest2NEW  26487  lmxrge0  26516  indf1ofs  26616  esumf1o  26638  esumfsup  26653  esumpcvgval  26661  esumcvg  26669  unelsiga  26711  cldssbrsiga  26735  sxbrsigalem1  26834  eulerpartlemsf  26876  eulerpartlems  26877  eulerpartlemb  26885  eulerpartgbij  26889  eulerpartlemgh  26895  fibp1  26918  ballotlemsf1o  27030  ballotlemrinv0  27049  sgnmulsgp  27067  plyrecld  27084  signslema  27097  signsvtn0  27105  signstfveq0  27112  eldmgm  27142  dmgmaddnn0  27147  lgamgulmlem2  27150  lgamcvg2  27175  regamcl  27181  relgamcl  27182  rpgamcl  27183  erdszelem8  27220  pconcon  27254  ptpcon  27256  txsconlem  27263  rescon  27269  cvmscld  27296  cvmliftmolem1  27304  cvmliftlem1  27308  cvmliftlem8  27315  cvmlift2lem9  27334  circum  27453  prodmolem2a  27581  fprodf1o  27593  fprodshft  27621  setlikespec  27782  wfrlem15  27872  onsuctop  28413  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  mbfresfi  28576  mbfposadd  28577  itg2addnclem  28581  itg2addnclem2  28582  itg2addnc  28584  itgaddnclem2  28589  itgaddnc  28590  iblsubnc  28591  itgmulc2nclem2  28597  itgmulc2nc  28598  itgabsnc  28599  bddiblnc  28600  ftc1cnnclem  28603  ftc1anclem1  28605  ftc1anclem2  28606  ftc1anclem4  28608  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  areacirclem2  28623  isfne4  28679  islocfin  28706  fnejoin2  28728  sdclem2  28776  geomcau  28793  ssbnd  28825  prdsbnd2  28832  divrngcl  28901  1idl  28964  inidl  28968  prnc  29005  ispridlc  29008  elrfi  29168  mzpaddmpt  29215  mzpmulmpt  29216  diophun  29250  elpell1qr2  29351  pellfundglb  29364  qirropth  29387  rmspecfund  29388  rmbaserp  29398  rmxnn  29432  jm2.27a  29492  jm2.27c  29494  fnwe2lem3  29543  lnmfg  29573  kercvrlsm  29574  lnmepi  29576  pwssplit4  29580  hbtlem5  29622  hbt  29624  rngunsnply  29668  acsfn1p  29694  iocmbl  29726  itgpowd  29728  rfcnpre1  29879  refsumcn  29890  rfcnpre2  29891  rfcnpre3  29893  rfcnpre4  29894  refsum2cnlem1  29897  mulc1cncfg  29908  stoweidlem9  29942  stoweidlem17  29950  stoweidlem19  29952  stoweidlem20  29953  stoweidlem23  29956  stoweidlem31  29964  stoweidlem41  29974  stoweidlem47  29980  stirlinglem3  30009  stirlinglem7  30013  stirlinglem8  30014  sigardiv  30035  afvelrn  30212  edgwlk  30432  extwwlkfablem1  30805  numclwlk2lem2f1o  30836  chfacfscmulgsum  31314  chfacfpmmulgsum  31318  chcoeffeqlem  31340  bnj1145  32284  riotasvd  32913  lkrlsp  33053  glbconN  33327  cvratlem  33371  llncvrlpln  33508  lplncvrlvol  33566  psubclsubN  33890  psubclinN  33898  4atexlemcnd  34022  cdleme23b  34300  cdlemk35  34862  dvaabl  34975  dia1elN  35005  diaintclN  35009  diasslssN  35010  dia2dimlem7  35021  dvadiaN  35079  dibintclN  35118  dihopelvalcpre  35199  dihsslss  35227  dih0rn  35235  dih1rn  35238  dihintcl  35295  dihmeetcl  35296  dochocss  35317  dochoccl  35320  dochsat  35334  dihsmsprn  35381  dochsnshp  35404  dochexmidlem6  35416  lcfl8b  35455  lclkrlem2g  35464  mapdpglem5N  35628  mapdpglem9  35631  mapdpglem14  35636  mapdpglem30a  35646  mapdpglem30b  35647  baerlem5amN  35667  baerlem5bmN  35668  baerlem5abmN  35669  mapdindp0  35670  mapdheq4lem  35682  mapdheq4  35683  mapdh6lem1N  35684  mapdh6lem2N  35685  mapdh7eN  35699  mapdh7cN  35700  mapdh7fN  35702  mapdh75e  35703  mapdh75fN  35706  mapdh8aa  35727  mapdh8d0N  35733  mapdh8d  35734  hdmap1eq2  35757  hdmap1eq4N  35758  hdmap1l6lem1  35759  hdmap1l6lem2  35760  hdmap1neglem1N  35779  hdmaprnlem7N  35809  hdmaprnlem17N  35817
  Copyright terms: Public domain W3C validator