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

Theorem eqeltrrd 2479
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 2409 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2478 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  3eltr3d  2484  tz7.7  4567  xpexr2  5267  fvmptdv2  5777  ffvresb  5859  2ndrn  6354  1st2ndbr  6355  elopabi  6371  cnvf1olem  6403  dftpos4  6457  riotasvd  6551  seqomlem4  6669  oneo  6783  oeordi  6789  oeeulem  6803  oeeui  6804  nnmordi  6833  nnneo  6853  th3qlem1  6969  disjen  7223  fnfi  7343  elfi2  7377  fisupcl  7428  ordiso2  7440  ordtypelem9  7451  hartogslem2  7468  unxpwdom2  7512  noinfep  7570  cantnflt  7583  cantnfp1lem3  7592  cantnflem1  7601  cantnflem3  7603  cantnf  7605  cnfcom3lem  7616  r1pwss  7666  r0weon  7850  alephfp  7945  dfac2a  7966  cfsmolem  8106  enfin2i  8157  ac6num  8315  ttukeylem7  8351  fpwwe2lem9  8469  canthp1lem2  8484  pwfseqlem4  8493  gchaleph2  8507  wunun  8541  r1tskina  8613  tskun  8617  gruen  8643  subf  9263  resubcl  9321  negcon1ad  9362  subeq0bd  9419  rimul  9947  peano2nn  9968  nn0nnaddcl  10208  elnn0nn  10218  elz2  10254  zsubcl  10275  zrevaddcl  10277  zdiv  10296  peano5uzi  10314  peano2uzr  10488  uzaddcl  10489  qsubcl  10549  qrevaddcl  10552  xov1plusxeqvd  10997  fseq1p1m1  11077  om2uzrani  11247  uzrdglem  11252  seqf1olem2  11318  expaddzlem  11378  expaddz  11379  expmulz  11381  zesq  11457  bcm1k  11561  bccl  11568  permnn  11572  hashcl  11594  hashf1lem2  11660  hashf1  11661  seqcoll  11667  shftuz  11839  ref  11872  imf  11873  crre  11874  rereb  11880  absf  12096  lo1res2  12311  o1res2  12312  o1add2  12372  o1mul2  12373  o1sub2  12374  lo1sub  12379  isercoll2  12417  summolem2a  12464  fsumf1o  12472  fsumcnv  12512  fsumshft  12518  geolim2  12603  ruclem12  12795  sqr2irrlem  12802  oexpneg  12866  3dvds  12867  bitsf1  12913  gcdf  12974  sqnprm  13053  fnum  13089  fden  13090  phimullem  13123  pc2dvds  13207  gzsubcl  13263  4sqlem5  13265  4sqlem9  13269  4sqlem10  13270  mul4sqlem  13276  mul4sq  13277  4sqlem11  13278  4sqlem13  13280  4sqlem16  13283  4sqlem17  13284  4sqlem18  13285  vdwlem5  13308  vdwlem8  13311  vdwlem9  13312  ramub1lem2  13350  firest  13615  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdshom  13644  prdsbascl  13660  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  mreincl  13779  ismred2  13783  mrcidb  13795  ssclem  13974  idffth  14085  ressffth  14090  coapm  14181  catciso  14217  evlfcl  14274  diag2cl  14298  hofcllem  14310  hofcl  14311  yonffthlem  14334  yoniso  14337  lubprop  14392  glbprop  14397  p0le  14427  ple1  14428  isglbd  14499  subsubm  14712  mhmima  14718  frmdss2  14763  mulgdir  14870  imasgrp2  14888  subgmulg  14913  issubg2  14914  subsubg  14918  cycsubgcl  14921  isnsg3  14929  ssnmz  14937  eqger  14945  ghmrn  14974  ghmnsgima  14984  conjsubg  14992  conjnmz  14994  subggim  15008  gass  15033  mndodconglem  15134  odsubdvds  15160  sylow1lem1  15187  sylow1lem3  15189  sylow1lem4  15190  pgpssslw  15203  sylow2a  15208  sylow2blem3  15211  slwhash  15213  fislw  15214  sylow3lem2  15217  sylow3lem4  15219  sylow3lem5  15220  sylow3lem6  15221  lsmub1x  15235  lsmub2x  15236  lsmsubm  15242  lsmmod  15262  lsmdisj2  15269  subgdisj1  15278  efginvrel2  15314  efgsres  15325  efgsfo  15326  efgredleme  15330  iscygodd  15453  prmcyg  15458  gsumzsubmcl  15478  gsum2d2lem  15502  pwsgsum  15508  dprdcntz  15521  dprddisj  15522  dprdw  15523  dprdfid  15530  dprdfinv  15532  dprdfadd  15533  dprdfsub  15534  dprdfeq0  15535  dprdf11  15536  dprdsubg  15537  dprdub  15538  dprdlub  15539  dprdres  15541  dprdss  15542  dprdf1o  15545  dmdprdsplitlem  15550  dprddisj2  15552  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2  15559  dpjfval  15568  dpjidcl  15571  ablfacrplem  15578  ablfacrp  15579  ablfac1c  15584  ablfac1eu  15586  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfaclem1  15594  pgpfaclem3  15596  ablfaclem3  15600  0unit  15740  irredneg  15770  irrednegb  15771  isdrng2  15800  subrgcrng  15827  subrgin  15846  subsubrg  15849  srngcl  15898  islmodd  15911  lssvancl1  15976  lss0cl  15978  lssvacl  15985  lssvscl  15986  lssvnegcl  15987  lssincl  15996  lmhmima  16078  lmhmrnlss  16081  lsslvec  16134  lspabs3  16148  lspdisj  16152  lspexch  16156  lsmcv  16168  lspsolv  16170  issubgrpd2  16215  issubrngd2  16217  rlmlvec  16232  lidl1el  16244  drngnidl  16255  2idlcpbl  16260  isassad  16337  issubassa2  16358  psrass1lem  16397  mvridlem  16438  mplsubrglem  16457  mplmonmul  16482  mplcoe3  16484  mplcoe2  16485  subrgasclcl  16514  mplmon2cl  16515  mplind  16517  zsssubrg  16712  cnsubrg  16714  gzrngunit  16719  zlpirlem1  16723  frgpcyg  16809  isphld  16840  css0  16871  pjfo  16897  unopn  16931  istps2OLD  16941  tsettps  16963  tgss2  17007  difopn  17053  incld  17062  iuncld  17064  indiscld  17110  mretopd  17111  resttop  17178  resttopon  17179  restfpw  17197  ordtbaslem  17206  ordtbas2  17209  ordtbas  17210  ordttopon  17211  ordtopn1  17212  ordtopn2  17213  ordtcld1  17215  ordtcld2  17216  ordtrest  17220  ordtrest2  17222  tgcn  17270  tgcnp  17271  cnpco  17285  cnt1  17368  cnrmnrm  17379  conndisj  17432  uncon  17445  2ndctop  17463  2ndcrest  17470  2ndcctbss  17471  2ndcomap  17474  dis2ndc  17476  restnlly  17498  islly2  17500  llyidm  17504  nllyidm  17505  dislly  17513  kgeni  17522  kgencmp2  17531  iskgen2  17533  kgencn2  17542  kgencn3  17543  elptr2  17559  ptbasfi  17566  txcld  17588  xkoccn  17604  txcn  17611  txdis  17617  txkgen  17637  xkopjcn  17641  xkococnlem  17644  cnmpt11  17648  cnmpt11f  17649  cnmpt1t  17650  cnmpt12  17652  cnmpt21  17656  cnmpt21f  17657  cnmpt2t  17658  cnmpt22  17659  cnmpt22f  17660  cnmpt1res  17661  cnmptkp  17665  cnmptk1  17666  cnmpt1k  17667  cnmptkk  17668  cnmptk1p  17670  cnmptk2  17671  cnmpt2k  17673  txcon  17674  basqtop  17696  tgqtop  17697  qtopeu  17701  qtoprest  17702  qtopomap  17703  qtopcmap  17704  r0cld  17723  ordthmeolem  17786  pt1hmeo  17791  ptcmpfi  17798  xkocnv  17799  xkohmeo  17800  fbdmn0  17819  trfil1  17871  trfil2  17872  trfg  17876  uzrest  17882  uzfbas  17883  trufil  17895  elfm3  17935  rnelfm  17938  fmfnfmlem2  17940  fmfnfm  17943  txflf  17991  alexsublem  18028  alexsub  18029  alexsubb  18030  ptcmplem3  18038  ptcmplem4  18039  cnmpt1plusg  18070  cnmpt2plusg  18071  istgp2  18074  oppgtgp  18081  symgtgp  18084  subgtgp  18088  subgntr  18089  opnsubg  18090  cldsubg  18093  tgpconcomp  18095  tgpt0  18101  divstgplem  18103  divstgphaus  18105  prdstmdd  18106  tsms0  18124  tsmsadd  18129  tsmsxplem1  18135  tsmsxplem2  18136  cnmpt1vsca  18176  cnmpt2vsca  18177  trust  18212  uspreg  18257  xpsdsval  18364  xmeter  18416  mscl  18444  xmscl  18445  blcld  18488  stdbdxmet  18498  met2ndci  18505  prdsxmslem2  18512  tmsxps  18519  metustidOLD  18542  metustid  18543  tngngpd  18647  tngnrg  18663  sranlm  18673  lssnlm  18689  lssnvc  18690  xrsxmet  18793  xrsblre  18795  zdis  18800  icccmplem2  18807  xrge0tsms  18818  cnmpt1ds  18826  cnmpt2ds  18827  cncfmpt1f  18896  negcncf  18901  negfcncf  18902  cnheiborlem  18932  evth  18937  evth2  18938  lebnumlem1  18939  lebnumlem3  18941  xlebnum  18943  copco  18996  pcopt  19000  pcopt2  19001  pi1addf  19025  pi1addval  19026  pi1cof  19037  pi1coghm  19039  isclmi  19055  cphsubrglem  19093  cphreccllem  19094  cphcjcl  19099  cphsqrcl2  19102  cphsqrcl3  19103  cphqss  19104  cphnmf  19111  reipcl  19113  ipcau2  19144  cnmpt1ip  19154  cnmpt2ip  19155  clsocv  19157  iscauf  19186  cmetcaulem  19194  lmle  19207  lmcau  19218  lssbn  19257  hlprlem  19274  ishl2  19277  minveclem3b  19282  pjthlem2  19292  ovolfcl  19316  ovoliunlem1  19351  ovolshftlem1  19358  ovolicc2lem3  19368  ovolicc2lem4  19369  shftmbl  19386  inmbl  19389  difmbl  19390  volinun  19393  volfiniun  19394  voliunlem3  19399  volsup  19403  icombl1  19410  icombl  19411  ioombl  19412  iccmbl  19413  uniioombllem3  19430  uniioombllem5  19432  uniiccmbl  19435  dyaddisjlem  19440  dyadmbl  19445  opnmbllem  19446  volcn  19451  vitalilem1  19453  vitalilem4  19456  mbfdm  19473  mbfimasn  19479  mbfdm2  19483  mbfmulc2lem  19492  mbfmulc2re  19493  mbfneg  19495  mbfpos  19496  mbfposr  19497  mbfposb  19498  ismbf3d  19499  mbfimaopnlem  19500  cncombf  19503  mbfaddlem  19505  mbfadd  19506  mbfsub  19507  mbfmulc2  19508  mbflimsup  19511  mbflimlem  19512  i1fima  19523  i1fima2  19524  i1fima2sn  19525  i1fd  19526  i1f0rn  19527  itg11  19536  i1faddlem  19538  i1fadd  19540  i1fmul  19541  itg1addlem2  19542  itg1addlem4  19544  itg1addlem5  19545  itg1mulc  19549  i1fres  19550  i1fposd  19552  i1fsub  19553  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flimlem  19567  mbfi1flim  19568  mbfmullem2  19569  mbfmul  19571  itg2const  19585  itg2const2  19586  itg2seq  19587  itg2splitlem  19593  itg2monolem1  19595  itg2mono  19598  itg2gt0  19605  itg2cnlem1  19606  iblss  19649  i1fibl  19652  itgitg1  19653  itgss3  19659  ibladd  19665  iblsub  19666  iblabs  19673  bddmulibl  19683  bddibl  19684  cnmptlimc  19730  limccnp  19731  limccnp2  19732  perfdvf  19743  dvcnp2  19759  cpnord  19774  cpncn  19775  cpnres  19776  dvcnvlem  19813  cmvth  19828  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  c1lip1  19834  c1lip2  19835  dvgt0lem1  19839  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem2  19855  dvcnvre  19856  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  ftc1lem1  19872  ftc1lem2  19873  ftc1a  19874  ftc1lem4  19876  ftc2  19881  ftc2ditglem  19882  ftc2ditg  19883  itgsubstlem  19885  evlsval2  19894  mpfconst  19912  mpfproj  19913  mpfaddcl  19916  mpfmulcl  19917  pf1const  19919  pf1id  19920  pf1subrg  19921  mpfpf1  19924  pf1addcl  19926  pf1mulcl  19927  pf1ind  19928  tdeglem4  19936  deg1pwle  19995  deg1submon1p  20028  plyco0  20064  elplyd  20074  plypow  20077  plyconst  20078  plypf1  20084  plysub  20091  dgrcolem1  20144  dgrcolem2  20145  vieta1lem1  20180  vieta1lem2  20181  iaa  20195  aalioulem1  20202  aalioulem4  20205  aaliou3lem6  20218  tayl0  20231  taylpfval  20234  taylthlem2  20243  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  mtestbdd  20274  mbfulm  20275  iblulm  20276  itgulm  20277  psercn2  20292  psercn  20295  abelthlem1  20300  abelthlem3  20302  abelth  20310  abelth2  20311  sincn  20313  coscn  20314  efcvx  20318  pige3  20378  cosne0  20385  tanregt0  20394  efif1olem4  20400  relogcl  20426  logdiv2  20465  logcn  20491  dvloglem  20492  logf1o2  20494  efopnlem2  20501  logccv  20507  cxpsqr  20547  loglesqr  20595  ang180lem1  20604  ang180lem2  20605  isosctrlem2  20616  angpined  20624  mcubic  20640  atanbnd  20719  atans2  20724  atantayl2  20731  atantayl3  20732  leibpi  20735  rlimcnp2  20758  efrlim  20761  cvxcl  20776  emcllem6  20792  fsumharmonic  20803  ftalem2  20809  ftalem7  20814  basellem2  20817  basellem3  20818  basellem5  20820  basellem9  20824  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  efchtdvds  20895  fsumdvdsmul  20933  chtublem  20948  fsumvma  20950  mersenne  20964  perfect  20968  dchrfi  20992  lgsne0  21070  lgseisenlem4  21089  lgsquadlem1  21091  2sqblem  21114  chebbnd2  21124  chto1lb  21125  rpvmasumlem  21134  dchrisumlem2  21137  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrmusumlem  21169  dchrvmasumlem  21170  rpvmasum  21173  rplogsum  21174  mudivsum  21177  mulog2sumlem3  21183  2vmadivsumlem  21187  selberglem2  21193  selberg2lem  21197  logdivbnd  21203  selberg3lem1  21204  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd2  21234  pntlemo  21254  iseupa  21640  ablomul  21896  ghgrp  21909  rngoablo2  21963  vcoprne  22011  nvi  22046  ipval2lem3  22154  ipval2lem6  22160  ipf  22165  ubthlem1  22325  minvecolem2  22330  minvecolem4a  22332  hhshsslem2  22721  shsel1  22776  pjoccl  22888  5oalem1  23109  5oalem5  23113  3oalem2  23118  pjrni  23157  hmopd  23478  imaelshi  23514  adjbdlnb  23540  adjsslnop  23543  bracnlnval  23570  hmopidmchi  23607  disjabrex  23977  disjabrexf  23978  xrge0tsmsd  24176  subofld  24198  metideq  24241  lmxrge0  24290  indf1ofs  24376  esumf1o  24398  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  unelsiga  24470  cldssbrsiga  24494  sxbrsigalem1  24588  ballotlemsf1o  24724  ballotlemrinv0  24743  eldmgm  24759  dmgmaddnn0  24764  lgamgulmlem2  24767  lgamcvg2  24792  regamcl  24798  relgamcl  24799  rpgamcl  24800  erdszelem8  24837  pconcon  24871  ptpcon  24873  txsconlem  24880  rescon  24886  cvmscld  24913  cvmliftmolem1  24921  cvmliftlem1  24925  cvmliftlem8  24932  cvmlift2lem9  24951  circum  25064  prodmolem2a  25213  fprodf1o  25225  fprodshft  25253  setlikespec  25401  wfrlem15  25484  onsuctop  26087  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  itgaddnclem2  26163  itgaddnc  26164  iblsubnc  26165  itgmulc2nclem2  26171  itgmulc2nc  26172  itgabsnc  26173  bddiblnc  26174  ftc1cnnclem  26177  areacirclem4  26183  isfne4  26239  islocfin  26266  fnejoin2  26288  unirep  26304  sdclem2  26336  geomcau  26355  ssbnd  26387  prdsbnd2  26394  divrngcl  26463  1idl  26526  inidl  26530  prnc  26567  ispridlc  26570  elrfi  26638  mzpaddmpt  26688  mzpmulmpt  26689  diophun  26722  elpell1qr2  26825  pellfundglb  26838  qirropth  26861  rmspecfund  26862  rmbaserp  26872  rmxnn  26906  jm2.27a  26966  jm2.27c  26968  fnwe2lem3  27017  lnmfg  27048  kercvrlsm  27049  lnmepi  27051  pwssplit4  27059  frlmgsum  27100  uvcresum  27110  frlmsplit2  27111  frlmup1  27118  hbtlem5  27200  hbt  27202  rngunsnply  27246  symggen  27279  psgnunilem1  27284  psgnunilem3  27287  acsfn1p  27375  rfcnpre1  27557  refsumcn  27568  rfcnpre2  27569  rfcnpre3  27571  rfcnpre4  27572  refsum2cnlem1  27575  mulc1cncfg  27588  stoweidlem9  27625  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem23  27639  stoweidlem31  27647  stoweidlem41  27657  stoweidlem47  27663  stirlinglem3  27692  stirlinglem7  27696  stirlinglem8  27697  sigardiv  27718  afvelrn  27899  bnj1145  29068  lkrlsp  29585  glbconN  29859  cvratlem  29903  llncvrlpln  30040  lplncvrlvol  30098  psubclsubN  30422  psubclinN  30430  4atexlemcnd  30554  cdleme23b  30832  cdlemk35  31394  dvaabl  31507  dia1elN  31537  diaintclN  31541  diasslssN  31542  dia2dimlem7  31553  dvadiaN  31611  dibintclN  31650  dihopelvalcpre  31731  dihsslss  31759  dih0rn  31767  dih1rn  31770  dihintcl  31827  dihmeetcl  31828  dochocss  31849  dochoccl  31852  dochsat  31866  dihsmsprn  31913  dochsnshp  31936  dochexmidlem6  31948  lcfl8b  31987  lclkrlem2g  31996  mapdpglem5N  32160  mapdpglem9  32163  mapdpglem14  32168  mapdpglem30a  32178  mapdpglem30b  32179  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdindp0  32202  mapdheq4lem  32214  mapdheq4  32215  mapdh6lem1N  32216  mapdh6lem2N  32217  mapdh7eN  32231  mapdh7cN  32232  mapdh7fN  32234  mapdh75e  32235  mapdh75fN  32238  mapdh8aa  32259  mapdh8d0N  32265  mapdh8d  32266  hdmap1eq2  32289  hdmap1eq4N  32290  hdmap1l6lem1  32291  hdmap1l6lem2  32292  hdmap1neglem1N  32311  hdmaprnlem7N  32341  hdmaprnlem17N  32349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator