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

Theorem eqeltrrd 2511
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 2441 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2510 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  3eltr3d  2516  tz7.7  4607  xpexr2  5308  fvmptdv2  5818  ffvresb  5900  2ndrn  6395  1st2ndbr  6396  elopabi  6412  cnvf1olem  6444  dftpos4  6498  riotasvd  6592  seqomlem4  6710  oneo  6824  oeordi  6830  oeeulem  6844  oeeui  6845  nnmordi  6874  nnneo  6894  th3qlem1  7010  disjen  7264  fnfi  7384  elfi2  7419  fisupcl  7472  ordiso2  7484  ordtypelem9  7495  hartogslem2  7512  unxpwdom2  7556  noinfep  7614  cantnflt  7627  cantnfp1lem3  7636  cantnflem1  7645  cantnflem3  7647  cantnf  7649  cnfcom3lem  7660  r1pwss  7710  r0weon  7894  alephfp  7989  dfac2a  8010  cfsmolem  8150  enfin2i  8201  ac6num  8359  ttukeylem7  8395  fpwwe2lem9  8513  canthp1lem2  8528  pwfseqlem4  8537  gchaleph2  8551  wunun  8585  r1tskina  8657  tskun  8661  gruen  8687  subf  9307  resubcl  9365  negcon1ad  9406  subeq0bd  9463  rimul  9991  peano2nn  10012  nn0nnaddcl  10252  elnn0nn  10262  elz2  10298  zsubcl  10319  zrevaddcl  10321  zdiv  10340  peano5uzi  10358  peano2uzr  10532  uzaddcl  10533  qsubcl  10593  qrevaddcl  10596  xov1plusxeqvd  11041  fseq1p1m1  11122  om2uzrani  11292  uzrdglem  11297  seqf1olem2  11363  expaddzlem  11423  expaddz  11424  expmulz  11426  zesq  11502  bcm1k  11606  bccl  11613  permnn  11617  hashcl  11639  hashf1lem2  11705  hashf1  11706  seqcoll  11712  shftuz  11884  ref  11917  imf  11918  crre  11919  rereb  11925  absf  12141  lo1res2  12356  o1res2  12357  o1add2  12417  o1mul2  12418  o1sub2  12419  lo1sub  12424  isercoll2  12462  summolem2a  12509  fsumf1o  12517  fsumcnv  12557  fsumshft  12563  geolim2  12648  ruclem12  12840  sqr2irrlem  12847  oexpneg  12911  3dvds  12912  bitsf1  12958  gcdf  13019  sqnprm  13098  fnum  13134  fden  13135  phimullem  13168  pc2dvds  13252  gzsubcl  13308  4sqlem5  13310  4sqlem9  13314  4sqlem10  13315  mul4sqlem  13321  mul4sq  13322  4sqlem11  13323  4sqlem13  13325  4sqlem16  13328  4sqlem17  13329  4sqlem18  13330  vdwlem5  13353  vdwlem8  13356  vdwlem9  13357  ramub1lem2  13395  firest  13660  prdsplusg  13681  prdsmulr  13682  prdsvsca  13683  prdshom  13689  prdsbascl  13705  xpsaddlem  13800  xpsvsca  13804  xpsle  13806  mreincl  13824  ismred2  13828  mrcidb  13840  ssclem  14019  idffth  14130  ressffth  14135  coapm  14226  catciso  14262  evlfcl  14319  diag2cl  14343  hofcllem  14355  hofcl  14356  yonffthlem  14379  yoniso  14382  lubprop  14437  glbprop  14442  p0le  14472  ple1  14473  isglbd  14544  subsubm  14757  mhmima  14763  frmdss2  14808  mulgdir  14915  imasgrp2  14933  subgmulg  14958  issubg2  14959  subsubg  14963  cycsubgcl  14966  isnsg3  14974  ssnmz  14982  eqger  14990  ghmrn  15019  ghmnsgima  15029  conjsubg  15037  conjnmz  15039  subggim  15053  gass  15078  mndodconglem  15179  odsubdvds  15205  sylow1lem1  15232  sylow1lem3  15234  sylow1lem4  15235  pgpssslw  15248  sylow2a  15253  sylow2blem3  15256  slwhash  15258  fislw  15259  sylow3lem2  15262  sylow3lem4  15264  sylow3lem5  15265  sylow3lem6  15266  lsmub1x  15280  lsmub2x  15281  lsmsubm  15287  lsmmod  15307  lsmdisj2  15314  subgdisj1  15323  efginvrel2  15359  efgsres  15370  efgsfo  15371  efgredleme  15375  iscygodd  15498  prmcyg  15503  gsumzsubmcl  15523  gsum2d2lem  15547  pwsgsum  15553  dprdcntz  15566  dprddisj  15567  dprdw  15568  dprdfid  15575  dprdfinv  15577  dprdfadd  15578  dprdfsub  15579  dprdfeq0  15580  dprdf11  15581  dprdsubg  15582  dprdub  15583  dprdlub  15584  dprdres  15586  dprdss  15587  dprdf1o  15590  dmdprdsplitlem  15595  dprddisj2  15597  dprd2dlem2  15598  dprd2dlem1  15599  dprd2da  15600  dmdprdsplit2  15604  dpjfval  15613  dpjidcl  15616  ablfacrplem  15623  ablfacrp  15624  ablfac1c  15629  ablfac1eu  15631  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfaclem1  15639  pgpfaclem3  15641  ablfaclem3  15645  0unit  15785  irredneg  15815  irrednegb  15816  isdrng2  15845  subrgcrng  15872  subrgin  15891  subsubrg  15894  srngcl  15943  islmodd  15956  lssvancl1  16021  lss0cl  16023  lssvacl  16030  lssvscl  16031  lssvnegcl  16032  lssincl  16041  lmhmima  16123  lmhmrnlss  16126  lsslvec  16179  lspabs3  16193  lspdisj  16197  lspexch  16201  lsmcv  16213  lspsolv  16215  issubgrpd2  16260  issubrngd2  16262  rlmlvec  16277  lidl1el  16289  drngnidl  16300  2idlcpbl  16305  isassad  16382  issubassa2  16403  psrass1lem  16442  mvridlem  16483  mplsubrglem  16502  mplmonmul  16527  mplcoe3  16529  mplcoe2  16530  subrgasclcl  16559  mplmon2cl  16560  mplind  16562  zsssubrg  16757  cnsubrg  16759  gzrngunit  16764  zlpirlem1  16768  frgpcyg  16854  isphld  16885  css0  16916  pjfo  16942  unopn  16976  istps2OLD  16986  tsettps  17008  tgss2  17052  difopn  17098  incld  17107  iuncld  17109  indiscld  17155  mretopd  17156  resttop  17224  resttopon  17225  restfpw  17243  ordtbaslem  17252  ordtbas2  17255  ordtbas  17256  ordttopon  17257  ordtopn1  17258  ordtopn2  17259  ordtcld1  17261  ordtcld2  17262  ordtrest  17266  ordtrest2  17268  tgcn  17316  tgcnp  17317  cnpco  17331  cnt1  17414  cnrmnrm  17425  conndisj  17479  uncon  17492  2ndctop  17510  2ndcrest  17517  2ndcctbss  17518  2ndcomap  17521  dis2ndc  17523  restnlly  17545  islly2  17547  llyidm  17551  nllyidm  17552  dislly  17560  kgeni  17569  kgencmp2  17578  iskgen2  17580  kgencn2  17589  kgencn3  17590  elptr2  17606  ptbasfi  17613  txcld  17635  xkoccn  17651  txcn  17658  txdis  17664  txkgen  17684  xkopjcn  17688  xkococnlem  17691  cnmpt11  17695  cnmpt11f  17696  cnmpt1t  17697  cnmpt12  17699  cnmpt21  17703  cnmpt21f  17704  cnmpt2t  17705  cnmpt22  17706  cnmpt22f  17707  cnmpt1res  17708  cnmptkp  17712  cnmptk1  17713  cnmpt1k  17714  cnmptkk  17715  cnmptk1p  17717  cnmptk2  17718  cnmpt2k  17720  txcon  17721  basqtop  17743  tgqtop  17744  qtopeu  17748  qtoprest  17749  qtopomap  17750  qtopcmap  17751  r0cld  17770  ordthmeolem  17833  pt1hmeo  17838  ptcmpfi  17845  xkocnv  17846  xkohmeo  17847  fbdmn0  17866  trfil1  17918  trfil2  17919  trfg  17923  uzrest  17929  uzfbas  17930  trufil  17942  elfm3  17982  rnelfm  17985  fmfnfmlem2  17987  fmfnfm  17990  txflf  18038  alexsublem  18075  alexsub  18076  alexsubb  18077  ptcmplem3  18085  ptcmplem4  18086  cnmpt1plusg  18117  cnmpt2plusg  18118  istgp2  18121  oppgtgp  18128  symgtgp  18131  subgtgp  18135  subgntr  18136  opnsubg  18137  cldsubg  18140  tgpconcomp  18142  tgpt0  18148  divstgplem  18150  divstgphaus  18152  prdstmdd  18153  tsms0  18171  tsmsadd  18176  tsmsxplem1  18182  tsmsxplem2  18183  cnmpt1vsca  18223  cnmpt2vsca  18224  trust  18259  uspreg  18304  xpsdsval  18411  xmeter  18463  mscl  18491  xmscl  18492  blcld  18535  stdbdxmet  18545  met2ndci  18552  prdsxmslem2  18559  tmsxps  18566  metustidOLD  18589  metustid  18590  tngngpd  18694  tngnrg  18710  sranlm  18720  lssnlm  18736  lssnvc  18737  xrsxmet  18840  xrsblre  18842  zdis  18847  icccmplem2  18854  xrge0tsms  18865  cnmpt1ds  18873  cnmpt2ds  18874  cncfmpt1f  18943  negcncf  18948  negfcncf  18949  cnheiborlem  18979  evth  18984  evth2  18985  lebnumlem1  18986  lebnumlem3  18988  xlebnum  18990  copco  19043  pcopt  19047  pcopt2  19048  pi1addf  19072  pi1addval  19073  pi1cof  19084  pi1coghm  19086  isclmi  19102  cphsubrglem  19140  cphreccllem  19141  cphcjcl  19146  cphsqrcl2  19149  cphsqrcl3  19150  cphqss  19151  cphnmf  19158  reipcl  19160  ipcau2  19191  cnmpt1ip  19201  cnmpt2ip  19202  clsocv  19204  iscauf  19233  cmetcaulem  19241  lmle  19254  lmcau  19265  lssbn  19304  hlprlem  19321  ishl2  19324  minveclem3b  19329  pjthlem2  19339  ovolfcl  19363  ovoliunlem1  19398  ovolshftlem1  19405  ovolicc2lem3  19415  ovolicc2lem4  19416  shftmbl  19433  inmbl  19436  difmbl  19437  volinun  19440  volfiniun  19441  voliunlem3  19446  volsup  19450  icombl1  19457  icombl  19458  ioombl  19459  iccmbl  19460  uniioombllem3  19477  uniioombllem5  19479  uniiccmbl  19482  dyaddisjlem  19487  dyadmbl  19492  opnmbllem  19493  volcn  19498  vitalilem1  19500  vitalilem4  19503  mbfdm  19520  mbfimasn  19526  mbfdm2  19530  mbfmulc2lem  19539  mbfmulc2re  19540  mbfneg  19542  mbfpos  19543  mbfposr  19544  mbfposb  19545  ismbf3d  19546  mbfimaopnlem  19547  cncombf  19550  mbfaddlem  19552  mbfadd  19553  mbfsub  19554  mbfmulc2  19555  mbflimsup  19558  mbflimlem  19559  i1fima  19570  i1fima2  19571  i1fima2sn  19572  i1fd  19573  i1f0rn  19574  itg11  19583  i1faddlem  19585  i1fadd  19587  i1fmul  19588  itg1addlem2  19589  itg1addlem4  19591  itg1addlem5  19592  itg1mulc  19596  i1fres  19597  i1fposd  19599  i1fsub  19600  itg1climres  19606  mbfi1fseqlem3  19609  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1flimlem  19614  mbfi1flim  19615  mbfmullem2  19616  mbfmul  19618  itg2const  19632  itg2const2  19633  itg2seq  19634  itg2splitlem  19640  itg2monolem1  19642  itg2mono  19645  itg2gt0  19652  itg2cnlem1  19653  iblss  19696  i1fibl  19699  itgitg1  19700  itgss3  19706  ibladd  19712  iblsub  19713  iblabs  19720  bddmulibl  19730  bddibl  19731  cnmptlimc  19777  limccnp  19778  limccnp2  19779  perfdvf  19790  dvcnp2  19806  cpnord  19821  cpncn  19822  cpnres  19823  dvcnvlem  19860  cmvth  19875  dvlip  19877  dvlipcn  19878  dvlip2  19879  c1liplem1  19880  c1lip1  19881  c1lip2  19882  dvgt0lem1  19886  lhop1lem  19897  lhop2  19899  lhop  19900  dvcnvrelem2  19902  dvcnvre  19903  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  ftc1lem1  19919  ftc1lem2  19920  ftc1a  19921  ftc1lem4  19923  ftc2  19928  ftc2ditglem  19929  ftc2ditg  19930  itgsubstlem  19932  evlsval2  19941  mpfconst  19959  mpfproj  19960  mpfaddcl  19963  mpfmulcl  19964  pf1const  19966  pf1id  19967  pf1subrg  19968  mpfpf1  19971  pf1addcl  19973  pf1mulcl  19974  pf1ind  19975  tdeglem4  19983  deg1pwle  20042  deg1submon1p  20075  plyco0  20111  elplyd  20121  plypow  20124  plyconst  20125  plypf1  20131  plysub  20138  dgrcolem1  20191  dgrcolem2  20192  vieta1lem1  20227  vieta1lem2  20228  iaa  20242  aalioulem1  20249  aalioulem4  20252  aaliou3lem6  20265  tayl0  20278  taylpfval  20281  taylthlem2  20290  ulmdvlem1  20316  ulmdvlem3  20318  mtest  20320  mtestbdd  20321  mbfulm  20322  iblulm  20323  itgulm  20324  psercn2  20339  psercn  20342  abelthlem1  20347  abelthlem3  20349  abelth  20357  abelth2  20358  sincn  20360  coscn  20361  efcvx  20365  pige3  20425  cosne0  20432  tanregt0  20441  efif1olem4  20447  relogcl  20473  logdiv2  20512  logcn  20538  dvloglem  20539  logf1o2  20541  efopnlem2  20548  logccv  20554  cxpsqr  20594  loglesqr  20642  ang180lem1  20651  ang180lem2  20652  isosctrlem2  20663  angpined  20671  mcubic  20687  atanbnd  20766  atans2  20771  atantayl2  20778  atantayl3  20779  leibpi  20782  rlimcnp2  20805  efrlim  20808  cvxcl  20823  emcllem6  20839  fsumharmonic  20850  ftalem2  20856  ftalem7  20861  basellem2  20864  basellem3  20865  basellem5  20867  basellem9  20871  ppiprm  20934  ppinprm  20935  chtprm  20936  chtnprm  20937  efchtdvds  20942  fsumdvdsmul  20980  chtublem  20995  fsumvma  20997  mersenne  21011  perfect  21015  dchrfi  21039  lgsne0  21117  lgseisenlem4  21136  lgsquadlem1  21138  2sqblem  21161  chebbnd2  21171  chto1lb  21172  rpvmasumlem  21181  dchrisumlem2  21184  dchrvmasumiflem1  21195  dchrvmasumiflem2  21196  dchrisum0fno1  21205  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lem1  21210  dchrisum0lem2a  21211  dchrisum0lem2  21212  dchrisum0lem3  21213  dchrmusumlem  21216  dchrvmasumlem  21217  rpvmasum  21220  rplogsum  21221  mudivsum  21224  mulog2sumlem3  21230  2vmadivsumlem  21234  selberglem2  21240  selberg2lem  21244  logdivbnd  21250  selberg3lem1  21251  selberg4lem1  21254  selberg4  21255  pntrsumo1  21259  selberg3r  21263  selberg4r  21264  selberg34r  21265  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntpbnd2  21281  pntlemo  21301  iseupa  21687  ablomul  21943  ghgrp  21956  rngoablo2  22010  vcoprne  22058  nvi  22093  ipval2lem3  22201  ipval2lem6  22207  ipf  22212  ubthlem1  22372  minvecolem2  22377  minvecolem4a  22379  hhshsslem2  22768  shsel1  22823  pjoccl  22935  5oalem1  23156  5oalem5  23160  3oalem2  23165  pjrni  23204  hmopd  23525  imaelshi  23561  adjbdlnb  23587  adjsslnop  23590  bracnlnval  23617  hmopidmchi  23654  disjabrex  24024  disjabrexf  24025  xrge0tsmsd  24223  subofld  24245  metideq  24288  lmxrge0  24337  indf1ofs  24423  esumf1o  24445  esumfsup  24460  esumpcvgval  24468  esumcvg  24476  unelsiga  24517  cldssbrsiga  24541  sxbrsigalem1  24635  ballotlemsf1o  24771  ballotlemrinv0  24790  eldmgm  24806  dmgmaddnn0  24811  lgamgulmlem2  24814  lgamcvg2  24839  regamcl  24845  relgamcl  24846  rpgamcl  24847  erdszelem8  24884  pconcon  24918  ptpcon  24920  txsconlem  24927  rescon  24933  cvmscld  24960  cvmliftmolem1  24968  cvmliftlem1  24972  cvmliftlem8  24979  cvmlift2lem9  24998  circum  25111  prodmolem2a  25260  fprodf1o  25272  fprodshft  25300  setlikespec  25462  wfrlem15  25552  onsuctop  26183  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  mbfresfi  26253  mbfposadd  26254  itg2addnclem  26256  itg2addnclem2  26257  itg2addnc  26259  itgaddnclem2  26264  itgaddnc  26265  iblsubnc  26266  itgmulc2nclem2  26272  itgmulc2nc  26273  itgabsnc  26274  bddiblnc  26275  ftc1cnnclem  26278  ftc1anclem1  26280  ftc1anclem2  26281  ftc1anclem4  26283  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  ftc2nc  26289  areacirclem2  26293  isfne4  26349  islocfin  26376  fnejoin2  26398  unirep  26414  sdclem2  26446  geomcau  26465  ssbnd  26497  prdsbnd2  26504  divrngcl  26573  1idl  26636  inidl  26640  prnc  26677  ispridlc  26680  elrfi  26748  mzpaddmpt  26798  mzpmulmpt  26799  diophun  26832  elpell1qr2  26935  pellfundglb  26948  qirropth  26971  rmspecfund  26972  rmbaserp  26982  rmxnn  27016  jm2.27a  27076  jm2.27c  27078  fnwe2lem3  27127  lnmfg  27157  kercvrlsm  27158  lnmepi  27160  pwssplit4  27168  frlmgsum  27209  uvcresum  27219  frlmsplit2  27220  frlmup1  27227  hbtlem5  27309  hbt  27311  rngunsnply  27355  symggen  27388  psgnunilem1  27393  psgnunilem3  27396  acsfn1p  27484  rfcnpre1  27666  refsumcn  27677  rfcnpre2  27678  rfcnpre3  27680  rfcnpre4  27681  refsum2cnlem1  27684  mulc1cncfg  27697  stoweidlem9  27734  stoweidlem17  27742  stoweidlem19  27744  stoweidlem20  27745  stoweidlem23  27748  stoweidlem31  27756  stoweidlem41  27766  stoweidlem47  27772  stirlinglem3  27801  stirlinglem7  27805  stirlinglem8  27806  sigardiv  27827  afvelrn  28008  bnj1145  29362  lkrlsp  29900  glbconN  30174  cvratlem  30218  llncvrlpln  30355  lplncvrlvol  30413  psubclsubN  30737  psubclinN  30745  4atexlemcnd  30869  cdleme23b  31147  cdlemk35  31709  dvaabl  31822  dia1elN  31852  diaintclN  31856  diasslssN  31857  dia2dimlem7  31868  dvadiaN  31926  dibintclN  31965  dihopelvalcpre  32046  dihsslss  32074  dih0rn  32082  dih1rn  32085  dihintcl  32142  dihmeetcl  32143  dochocss  32164  dochoccl  32167  dochsat  32181  dihsmsprn  32228  dochsnshp  32251  dochexmidlem6  32263  lcfl8b  32302  lclkrlem2g  32311  mapdpglem5N  32475  mapdpglem9  32478  mapdpglem14  32483  mapdpglem30a  32493  mapdpglem30b  32494  baerlem5amN  32514  baerlem5bmN  32515  baerlem5abmN  32516  mapdindp0  32517  mapdheq4lem  32529  mapdheq4  32530  mapdh6lem1N  32531  mapdh6lem2N  32532  mapdh7eN  32546  mapdh7cN  32547  mapdh7fN  32549  mapdh75e  32550  mapdh75fN  32553  mapdh8aa  32574  mapdh8d0N  32580  mapdh8d  32581  hdmap1eq2  32604  hdmap1eq4N  32605  hdmap1l6lem1  32606  hdmap1l6lem2  32607  hdmap1neglem1N  32626  hdmaprnlem7N  32656  hdmaprnlem17N  32664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator