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

Theorem eqeltrrd 2462
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 2392 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2461 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717
This theorem is referenced by:  3eltr3d  2467  tz7.7  4548  xpexr2  5248  fvmptdv2  5757  ffvresb  5839  2ndrn  6334  1st2ndbr  6335  elopabi  6351  cnvf1olem  6383  dftpos4  6434  riotasvd  6528  seqomlem4  6646  oneo  6760  oeordi  6766  oeeulem  6780  oeeui  6781  nnmordi  6810  nnneo  6830  th3qlem1  6946  disjen  7200  fnfi  7320  elfi2  7354  fisupcl  7405  ordiso2  7417  ordtypelem9  7428  hartogslem2  7445  unxpwdom2  7489  noinfep  7547  cantnflt  7560  cantnfp1lem3  7569  cantnflem1  7578  cantnflem3  7580  cantnf  7582  cnfcom3lem  7593  r1pwss  7643  r0weon  7827  alephfp  7922  dfac2a  7943  cfsmolem  8083  enfin2i  8134  ac6num  8292  ttukeylem7  8328  fpwwe2lem9  8446  canthp1lem2  8461  pwfseqlem4  8470  gchaleph2  8484  wunun  8518  r1tskina  8590  tskun  8594  gruen  8620  subf  9239  resubcl  9297  negcon1ad  9338  subeq0bd  9395  rimul  9923  peano2nn  9944  nn0nnaddcl  10184  elnn0nn  10194  elz2  10230  zsubcl  10251  zrevaddcl  10253  zdiv  10272  peano5uzi  10290  peano2uzr  10464  uzaddcl  10465  qsubcl  10525  qrevaddcl  10528  xov1plusxeqvd  10973  fseq1p1m1  11052  om2uzrani  11219  uzrdglem  11224  seqf1olem2  11290  expaddzlem  11350  expaddz  11351  expmulz  11353  zesq  11429  bcm1k  11533  bccl  11540  permnn  11544  hashcl  11566  hashf1lem2  11632  hashf1  11633  seqcoll  11639  shftuz  11811  ref  11844  imf  11845  crre  11846  rereb  11852  absf  12068  lo1res2  12283  o1res2  12284  o1add2  12344  o1mul2  12345  o1sub2  12346  lo1sub  12351  isercoll2  12389  summolem2a  12436  fsumf1o  12444  fsumcnv  12484  fsumshft  12490  geolim2  12575  ruclem12  12767  sqr2irrlem  12774  oexpneg  12838  3dvds  12839  bitsf1  12885  gcdf  12946  sqnprm  13025  fnum  13061  fden  13062  phimullem  13095  pc2dvds  13179  gzsubcl  13235  4sqlem5  13237  4sqlem9  13241  4sqlem10  13242  mul4sqlem  13248  mul4sq  13249  4sqlem11  13250  4sqlem13  13252  4sqlem16  13255  4sqlem17  13256  4sqlem18  13257  vdwlem5  13280  vdwlem8  13283  vdwlem9  13284  ramub1lem2  13322  firest  13587  prdsplusg  13608  prdsmulr  13609  prdsvsca  13610  prdshom  13616  prdsbascl  13632  xpsaddlem  13727  xpsvsca  13731  xpsle  13733  mreincl  13751  ismred2  13755  mrcidb  13767  ssclem  13946  idffth  14057  ressffth  14062  coapm  14153  catciso  14189  evlfcl  14246  diag2cl  14270  hofcllem  14282  hofcl  14283  yonffthlem  14306  yoniso  14309  lubprop  14364  glbprop  14369  p0le  14399  ple1  14400  isglbd  14471  subsubm  14684  mhmima  14690  frmdss2  14735  mulgdir  14842  imasgrp2  14860  subgmulg  14885  issubg2  14886  subsubg  14890  cycsubgcl  14893  isnsg3  14901  ssnmz  14909  eqger  14917  ghmrn  14946  ghmnsgima  14956  conjsubg  14964  conjnmz  14966  subggim  14980  gass  15005  mndodconglem  15106  odsubdvds  15132  sylow1lem1  15159  sylow1lem3  15161  sylow1lem4  15162  pgpssslw  15175  sylow2a  15180  sylow2blem3  15183  slwhash  15185  fislw  15186  sylow3lem2  15189  sylow3lem4  15191  sylow3lem5  15192  sylow3lem6  15193  lsmub1x  15207  lsmub2x  15208  lsmsubm  15214  lsmmod  15234  lsmdisj2  15241  subgdisj1  15250  efginvrel2  15286  efgsres  15297  efgsfo  15298  efgredleme  15302  iscygodd  15425  prmcyg  15430  gsumzsubmcl  15450  gsum2d2lem  15474  pwsgsum  15480  dprdcntz  15493  dprddisj  15494  dprdw  15495  dprdfid  15502  dprdfinv  15504  dprdfadd  15505  dprdfsub  15506  dprdfeq0  15507  dprdf11  15508  dprdsubg  15509  dprdub  15510  dprdlub  15511  dprdres  15513  dprdss  15514  dprdf1o  15517  dmdprdsplitlem  15522  dprddisj2  15524  dprd2dlem2  15525  dprd2dlem1  15526  dprd2da  15527  dmdprdsplit2  15531  dpjfval  15540  dpjidcl  15543  ablfacrplem  15550  ablfacrp  15551  ablfac1c  15556  ablfac1eu  15558  pgpfac1lem3a  15561  pgpfac1lem3  15562  pgpfaclem1  15566  pgpfaclem3  15568  ablfaclem3  15572  0unit  15712  irredneg  15742  irrednegb  15743  isdrng2  15772  subrgcrng  15799  subrgin  15818  subsubrg  15821  srngcl  15870  islmodd  15883  lssvancl1  15948  lss0cl  15950  lssvacl  15957  lssvscl  15958  lssvnegcl  15959  lssincl  15968  lmhmima  16050  lmhmrnlss  16053  lsslvec  16106  lspabs3  16120  lspdisj  16124  lspexch  16128  lsmcv  16140  lspsolv  16142  issubgrpd2  16187  issubrngd2  16189  rlmlvec  16204  lidl1el  16216  drngnidl  16227  2idlcpbl  16232  isassad  16309  issubassa2  16330  psrass1lem  16369  mvridlem  16410  mplsubrglem  16429  mplmonmul  16454  mplcoe3  16456  mplcoe2  16457  subrgasclcl  16486  mplmon2cl  16487  mplind  16489  zsssubrg  16680  cnsubrg  16682  gzrngunit  16687  zlpirlem1  16691  frgpcyg  16777  isphld  16808  css0  16839  pjfo  16865  unopn  16899  istps2OLD  16909  tsettps  16931  tgss2  16975  difopn  17021  incld  17030  iuncld  17032  indiscld  17078  mretopd  17079  resttop  17146  resttopon  17147  restfpw  17165  ordtbaslem  17174  ordtbas2  17177  ordtbas  17178  ordttopon  17179  ordtopn1  17180  ordtopn2  17181  ordtcld1  17183  ordtcld2  17184  ordtrest  17188  ordtrest2  17190  tgcn  17238  tgcnp  17239  cnpco  17253  cnt1  17336  cnrmnrm  17347  conndisj  17400  uncon  17413  2ndctop  17431  2ndcrest  17438  2ndcctbss  17439  2ndcomap  17442  dis2ndc  17444  restnlly  17466  islly2  17468  llyidm  17472  nllyidm  17473  dislly  17481  kgeni  17490  kgencmp2  17499  iskgen2  17501  kgencn2  17510  kgencn3  17511  elptr2  17527  ptbasfi  17534  txcld  17556  xkoccn  17572  txcn  17579  txdis  17585  txkgen  17605  xkopjcn  17609  xkococnlem  17612  cnmpt11  17616  cnmpt11f  17617  cnmpt1t  17618  cnmpt12  17620  cnmpt21  17624  cnmpt21f  17625  cnmpt2t  17626  cnmpt22  17627  cnmpt22f  17628  cnmpt1res  17629  cnmptkp  17633  cnmptk1  17634  cnmpt1k  17635  cnmptkk  17636  cnmptk1p  17638  cnmptk2  17639  cnmpt2k  17641  txcon  17642  basqtop  17664  tgqtop  17665  qtopeu  17669  qtoprest  17670  qtopomap  17671  qtopcmap  17672  r0cld  17691  ordthmeolem  17754  pt1hmeo  17759  ptcmpfi  17766  xkocnv  17767  xkohmeo  17768  fbdmn0  17787  trfil1  17839  trfil2  17840  trfg  17844  uzrest  17850  uzfbas  17851  trufil  17863  elfm3  17903  rnelfm  17906  fmfnfmlem2  17908  fmfnfm  17911  txflf  17959  alexsublem  17996  alexsub  17997  alexsubb  17998  ptcmplem3  18006  ptcmplem4  18007  cnmpt1plusg  18038  cnmpt2plusg  18039  istgp2  18042  oppgtgp  18049  symgtgp  18052  subgtgp  18056  subgntr  18057  opnsubg  18058  cldsubg  18061  tgpconcomp  18063  tgpt0  18069  divstgplem  18071  divstgphaus  18073  prdstmdd  18074  tsms0  18092  tsmsadd  18097  tsmsxplem1  18103  tsmsxplem2  18104  cnmpt1vsca  18144  cnmpt2vsca  18145  trust  18180  uspreg  18225  xpsdsval  18319  xmeter  18353  mscl  18381  xmscl  18382  blcld  18425  stdbdxmet  18435  met2ndci  18442  prdsxmslem2  18449  tmsxps  18456  metustid  18474  tngngpd  18565  tngnrg  18581  sranlm  18591  lssnlm  18607  lssnvc  18608  xrsxmet  18711  xrsblre  18713  zdis  18718  icccmplem2  18725  xrge0tsms  18736  cnmpt1ds  18744  cnmpt2ds  18745  cncfmpt1f  18814  negcncf  18819  negfcncf  18820  cnheiborlem  18850  evth  18855  evth2  18856  lebnumlem1  18857  lebnumlem3  18859  xlebnum  18861  copco  18914  pcopt  18918  pcopt2  18919  pi1addf  18943  pi1addval  18944  pi1cof  18955  pi1coghm  18957  isclmi  18973  cphsubrglem  19011  cphreccllem  19012  cphcjcl  19017  cphsqrcl2  19020  cphsqrcl3  19021  cphqss  19022  cphnmf  19029  reipcl  19031  ipcau2  19062  cnmpt1ip  19072  cnmpt2ip  19073  clsocv  19075  iscauf  19104  cmetcaulem  19112  lmle  19125  lmcau  19136  lssbn  19173  hlprlem  19188  ishl2  19191  minveclem3b  19196  pjthlem2  19206  ovolfcl  19230  ovoliunlem1  19265  ovolshftlem1  19272  ovolicc2lem3  19282  ovolicc2lem4  19283  shftmbl  19300  inmbl  19303  difmbl  19304  volinun  19307  volfiniun  19308  voliunlem3  19313  volsup  19317  icombl1  19324  icombl  19325  ioombl  19326  iccmbl  19327  uniioombllem3  19344  uniioombllem5  19346  uniiccmbl  19349  dyaddisjlem  19354  dyadmbl  19359  opnmbllem  19360  volcn  19365  vitalilem1  19367  vitalilem4  19370  mbfdm  19387  mbfimasn  19393  mbfdm2  19397  mbfmulc2lem  19406  mbfmulc2re  19407  mbfneg  19409  mbfpos  19410  mbfposr  19411  mbfposb  19412  ismbf3d  19413  mbfimaopnlem  19414  cncombf  19417  mbfaddlem  19419  mbfadd  19420  mbfsub  19421  mbfmulc2  19422  mbflimsup  19425  mbflimlem  19426  i1fima  19437  i1fima2  19438  i1fima2sn  19439  i1fd  19440  i1f0rn  19441  itg11  19450  i1faddlem  19452  i1fadd  19454  i1fmul  19455  itg1addlem2  19456  itg1addlem4  19458  itg1addlem5  19459  itg1mulc  19463  i1fres  19464  i1fposd  19466  i1fsub  19467  itg1climres  19473  mbfi1fseqlem3  19476  mbfi1fseqlem4  19477  mbfi1fseqlem5  19478  mbfi1flimlem  19481  mbfi1flim  19482  mbfmullem2  19483  mbfmul  19485  itg2const  19499  itg2const2  19500  itg2seq  19501  itg2splitlem  19507  itg2monolem1  19509  itg2mono  19512  itg2gt0  19519  itg2cnlem1  19520  iblss  19563  i1fibl  19566  itgitg1  19567  itgss3  19573  ibladd  19579  iblsub  19580  iblabs  19587  bddmulibl  19597  bddibl  19598  cnmptlimc  19644  limccnp  19645  limccnp2  19646  perfdvf  19657  dvcnp2  19673  cpnord  19688  cpncn  19689  cpnres  19690  dvcnvlem  19727  cmvth  19742  dvlip  19744  dvlipcn  19745  dvlip2  19746  c1liplem1  19747  c1lip1  19748  c1lip2  19749  dvgt0lem1  19753  lhop1lem  19764  lhop2  19766  lhop  19767  dvcnvrelem2  19769  dvcnvre  19770  dvfsumle  19772  dvfsumabs  19774  dvfsumlem2  19778  ftc1lem1  19786  ftc1lem2  19787  ftc1a  19788  ftc1lem4  19790  ftc2  19795  ftc2ditglem  19796  ftc2ditg  19797  itgsubstlem  19799  evlsval2  19808  mpfconst  19826  mpfproj  19827  mpfaddcl  19830  mpfmulcl  19831  pf1const  19833  pf1id  19834  pf1subrg  19835  mpfpf1  19838  pf1addcl  19840  pf1mulcl  19841  pf1ind  19842  tdeglem4  19850  deg1pwle  19909  deg1submon1p  19942  plyco0  19978  elplyd  19988  plypow  19991  plyconst  19992  plypf1  19998  plysub  20005  dgrcolem1  20058  dgrcolem2  20059  vieta1lem1  20094  vieta1lem2  20095  iaa  20109  aalioulem1  20116  aalioulem4  20119  aaliou3lem6  20132  tayl0  20145  taylpfval  20148  taylthlem2  20157  ulmdvlem1  20183  ulmdvlem3  20185  mtest  20187  mtestbdd  20188  mbfulm  20189  iblulm  20190  itgulm  20191  psercn2  20206  psercn  20209  abelthlem1  20214  abelthlem3  20216  abelth  20224  abelth2  20225  sincn  20227  coscn  20228  efcvx  20232  pige3  20292  cosne0  20299  tanregt0  20308  efif1olem4  20314  relogcl  20340  logdiv2  20379  logcn  20405  dvloglem  20406  logf1o2  20408  efopnlem2  20415  logccv  20421  cxpsqr  20461  loglesqr  20509  ang180lem1  20518  ang180lem2  20519  isosctrlem2  20530  angpined  20538  mcubic  20554  atanbnd  20633  atans2  20638  atantayl2  20645  atantayl3  20646  leibpi  20649  rlimcnp2  20672  efrlim  20675  cvxcl  20690  emcllem6  20706  fsumharmonic  20717  ftalem2  20723  ftalem7  20728  basellem2  20731  basellem3  20732  basellem5  20734  basellem9  20738  ppiprm  20801  ppinprm  20802  chtprm  20803  chtnprm  20804  efchtdvds  20809  fsumdvdsmul  20847  chtublem  20862  fsumvma  20864  mersenne  20878  perfect  20882  dchrfi  20906  lgsne0  20984  lgseisenlem4  21003  lgsquadlem1  21005  2sqblem  21028  chebbnd2  21038  chto1lb  21039  rpvmasumlem  21048  dchrisumlem2  21051  dchrvmasumiflem1  21062  dchrvmasumiflem2  21063  dchrisum0fno1  21072  rpvmasum2  21073  dchrisum0re  21074  dchrisum0lem1  21077  dchrisum0lem2a  21078  dchrisum0lem2  21079  dchrisum0lem3  21080  dchrmusumlem  21083  dchrvmasumlem  21084  rpvmasum  21087  rplogsum  21088  mudivsum  21091  mulog2sumlem3  21097  2vmadivsumlem  21101  selberglem2  21107  selberg2lem  21111  logdivbnd  21117  selberg3lem1  21118  selberg4lem1  21121  selberg4  21122  pntrsumo1  21126  selberg3r  21130  selberg4r  21131  selberg34r  21132  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntpbnd2  21148  pntlemo  21168  iseupa  21535  ablomul  21791  ghgrp  21804  rngoablo2  21858  vcoprne  21906  nvi  21941  ipval2lem3  22049  ipval2lem6  22055  ipf  22060  ubthlem1  22220  minvecolem2  22225  minvecolem4a  22227  hhshsslem2  22616  shsel1  22671  pjoccl  22783  5oalem1  23004  5oalem5  23008  3oalem2  23013  pjrni  23052  hmopd  23373  imaelshi  23409  adjbdlnb  23435  adjsslnop  23438  bracnlnval  23465  hmopidmchi  23502  disjabrex  23868  disjabrexf  23869  xrge0tsmsd  24052  subofld  24071  lmxrge0  24141  indf1ofs  24219  esumf1o  24241  esumfsup  24256  esumpcvgval  24264  esumcvg  24272  unelsiga  24313  cldssbrsiga  24337  sxbrsigalem1  24429  ballotlemsf1o  24550  ballotlemrinv0  24569  eldmgm  24585  dmgmaddnn0  24590  lgamgulmlem2  24593  lgamcvg2  24618  regamcl  24624  relgamcl  24625  rpgamcl  24626  erdszelem8  24663  pconcon  24697  ptpcon  24699  txsconlem  24706  rescon  24712  cvmscld  24739  cvmliftmolem1  24747  cvmliftlem1  24751  cvmliftlem8  24758  cvmlift2lem9  24777  circum  24890  prodmolem2a  25039  fprodf1o  25051  fprodshft  25079  setlikespec  25211  wfrlem15  25294  onsuctop  25897  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  itgaddnclem2  25964  itgaddnc  25965  iblsubnc  25966  itgmulc2nclem2  25972  itgmulc2nc  25973  itgabsnc  25974  bddiblnc  25975  ftc1cnnclem  25978  areacirclem4  25984  isfne4  26040  islocfin  26067  fnejoin2  26089  unirep  26105  sdclem2  26137  geomcau  26156  ssbnd  26188  prdsbnd2  26195  divrngcl  26264  1idl  26327  inidl  26331  prnc  26368  ispridlc  26371  elrfi  26439  mzpaddmpt  26489  mzpmulmpt  26490  diophun  26523  elpell1qr2  26626  pellfundglb  26639  qirropth  26662  rmspecfund  26663  rmbaserp  26673  rmxnn  26707  jm2.27a  26767  jm2.27c  26769  fnwe2lem3  26818  lnmfg  26849  kercvrlsm  26850  lnmepi  26852  pwssplit4  26860  frlmgsum  26901  uvcresum  26911  frlmsplit2  26912  frlmup1  26919  hbtlem5  27001  hbt  27003  rngunsnply  27047  symggen  27080  psgnunilem1  27085  psgnunilem3  27088  acsfn1p  27176  rfcnpre1  27358  refsumcn  27369  rfcnpre2  27370  rfcnpre3  27372  rfcnpre4  27373  refsum2cnlem1  27376  mulc1cncfg  27389  stoweidlem9  27426  stoweidlem17  27434  stoweidlem19  27436  stoweidlem20  27437  stoweidlem23  27440  stoweidlem31  27448  stoweidlem41  27458  stoweidlem47  27464  stirlinglem3  27493  stirlinglem7  27497  stirlinglem8  27498  sigardiv  27519  afvelrn  27701  bnj1145  28700  lkrlsp  29217  glbconN  29491  cvratlem  29535  llncvrlpln  29672  lplncvrlvol  29730  psubclsubN  30054  psubclinN  30062  4atexlemcnd  30186  cdleme23b  30464  cdlemk35  31026  dvaabl  31139  dia1elN  31169  diaintclN  31173  diasslssN  31174  dia2dimlem7  31185  dvadiaN  31243  dibintclN  31282  dihopelvalcpre  31363  dihsslss  31391  dih0rn  31399  dih1rn  31402  dihintcl  31459  dihmeetcl  31460  dochocss  31481  dochoccl  31484  dochsat  31498  dihsmsprn  31545  dochsnshp  31568  dochexmidlem6  31580  lcfl8b  31619  lclkrlem2g  31628  mapdpglem5N  31792  mapdpglem9  31795  mapdpglem14  31800  mapdpglem30a  31810  mapdpglem30b  31811  baerlem5amN  31831  baerlem5bmN  31832  baerlem5abmN  31833  mapdindp0  31834  mapdheq4lem  31846  mapdheq4  31847  mapdh6lem1N  31848  mapdh6lem2N  31849  mapdh7eN  31863  mapdh7cN  31864  mapdh7fN  31866  mapdh75e  31867  mapdh75fN  31870  mapdh8aa  31891  mapdh8d0N  31897  mapdh8d  31898  hdmap1eq2  31921  hdmap1eq4N  31922  hdmap1l6lem1  31923  hdmap1l6lem2  31924  hdmap1neglem1N  31943  hdmaprnlem7N  31973  hdmaprnlem17N  31981
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 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380  df-clel 2383
  Copyright terms: Public domain W3C validator