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

Theorem eqeltrrd 2433
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 2363 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2432 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710
This theorem is referenced by:  3eltr3d  2438  tz7.7  4500  xpexr2  5197  fvmptdv2  5696  ffvresb  5773  2ndrn  6255  1st2ndbr  6256  elopabi  6272  cnvf1olem  6303  dftpos4  6340  riotasvd  6434  seqomlem4  6552  oneo  6666  oeordi  6672  oeeulem  6686  oeeui  6687  nnmordi  6716  nnneo  6736  th3qlem1  6852  disjen  7106  fnfi  7224  elfi2  7258  marypha2  7282  fisupcl  7308  ordiso2  7320  ordtypelem9  7331  hartogslem2  7348  unxpwdom2  7392  noinfep  7450  cantnflt  7463  cantnfp1lem3  7472  cantnflem1  7481  cantnflem3  7483  cantnf  7485  cnfcom3lem  7496  r1pwss  7546  r0weon  7730  alephfp  7825  dfac2a  7846  cfsmolem  7986  enfin2i  8037  ac6num  8196  ttukeylem7  8232  fpwwe2lem9  8350  canthp1lem2  8365  pwfseqlem4  8374  gchaleph2  8388  wunun  8422  r1tskina  8494  tskun  8498  gruen  8524  subf  9143  resubcl  9201  negcon1ad  9242  subeq0bd  9299  rimul  9827  peano2nn  9848  nn0nnaddcl  10088  elnn0nn  10098  elz2  10132  zsubcl  10153  zrevaddcl  10155  zdiv  10174  peano5uzi  10192  peano2uzr  10366  uzaddcl  10367  qsubcl  10427  qrevaddcl  10430  icoshftf1o  10851  lincmb01cmp  10869  xov1plusxeqvd  10872  fseq1p1m1  10949  om2uzrani  11107  uzrdglem  11112  seqf1olem2  11178  expaddzlem  11238  expaddz  11239  expmulz  11241  zesq  11317  bcm1k  11420  bccl  11427  permnn  11429  hashcl  11443  hashf1lem2  11490  hashf1  11491  seqcoll  11497  shftuz  11660  ref  11693  imf  11694  crre  11695  rereb  11701  absf  11917  lo1res2  12132  o1res2  12133  o1add2  12193  o1mul2  12194  o1sub2  12195  lo1sub  12200  isercoll2  12238  summolem2a  12285  fsumf1o  12293  fsumcnv  12333  fsumshft  12339  geolim2  12424  ruclem12  12616  sqr2irrlem  12623  oexpneg  12687  3dvds  12688  bitsf1  12734  gcdf  12795  sqnprm  12874  fnum  12910  fden  12911  phimullem  12944  pc2dvds  13028  gzsubcl  13084  4sqlem5  13086  4sqlem9  13090  4sqlem10  13091  mul4sqlem  13097  mul4sq  13098  4sqlem11  13099  4sqlem13  13101  4sqlem16  13104  4sqlem17  13105  4sqlem18  13106  vdwlem5  13129  vdwlem8  13132  vdwlem9  13133  ramub1lem2  13171  firest  13436  prdsplusg  13457  prdsmulr  13458  prdsvsca  13459  prdshom  13465  prdsbascl  13481  xpsaddlem  13576  xpsvsca  13580  xpsle  13582  mreincl  13600  ismred2  13604  mrcidb  13616  ssclem  13795  idffth  13906  ressffth  13911  coapm  14002  catciso  14038  evlfcl  14095  curfpropd  14106  diag2cl  14119  hofcllem  14131  hofcl  14132  yonffthlem  14155  yoniso  14158  lubprop  14213  glbprop  14218  p0le  14248  ple1  14249  isglbd  14320  subsubm  14533  mhmima  14539  frmdss2  14584  mulgdir  14691  imasgrp2  14709  subgmulg  14734  issubg2  14735  subsubg  14739  cycsubgcl  14742  isnsg3  14750  ssnmz  14758  eqger  14766  ghmrn  14795  ghmnsgima  14805  conjsubg  14813  conjnmz  14815  subggim  14829  gass  14854  mndodconglem  14955  odsubdvds  14981  sylow1lem1  15008  sylow1lem3  15010  sylow1lem4  15011  pgpssslw  15024  sylow2a  15029  sylow2blem3  15032  slwhash  15034  fislw  15035  sylow3lem2  15038  sylow3lem4  15040  sylow3lem5  15041  sylow3lem6  15042  lsmub1x  15056  lsmub2x  15057  lsmsubm  15063  lsmmod  15083  lsmdisj2  15090  subgdisj1  15099  efginvrel2  15135  efgsres  15146  efgsfo  15147  efgredleme  15151  iscygodd  15274  prmcyg  15279  gsumzsubmcl  15299  gsum2d2lem  15323  pwsgsum  15329  dprdcntz  15342  dprddisj  15343  dprdw  15344  dprdfid  15351  dprdfinv  15353  dprdfadd  15354  dprdfsub  15355  dprdfeq0  15356  dprdf11  15357  dprdsubg  15358  dprdub  15359  dprdlub  15360  dprdres  15362  dprdss  15363  dprdf1o  15366  dmdprdsplitlem  15371  dprddisj2  15373  dprd2dlem2  15374  dprd2dlem1  15375  dprd2da  15376  dmdprdsplit2  15380  dpjfval  15389  dpjidcl  15392  ablfacrplem  15399  ablfacrp  15400  ablfac1c  15405  ablfac1eu  15407  pgpfac1lem3a  15410  pgpfac1lem3  15411  pgpfaclem1  15415  pgpfaclem3  15417  ablfaclem3  15421  0unit  15561  irredneg  15591  irrednegb  15592  isdrng2  15621  subrgcrng  15648  subrgin  15667  subsubrg  15670  srngcl  15719  islmodd  15732  lssvancl1  15801  lss0cl  15803  lssvacl  15810  lssvscl  15811  lssvnegcl  15812  lssincl  15821  lmhmima  15903  lmhmrnlss  15906  lspprabs  15947  lsslvec  15959  lspabs3  15973  lspdisj  15977  lspexch  15981  lsmcv  15993  lspsolv  15995  issubgrpd2  16040  issubrngd2  16042  rlmlvec  16057  lidl1el  16069  drngnidl  16080  2idlcpbl  16085  isassad  16162  issubassa2  16183  psrass1lem  16222  mvridlem  16263  mplsubrglem  16282  mplmonmul  16307  mplcoe3  16309  mplcoe2  16310  subrgasclcl  16339  mplmon2cl  16340  mplind  16342  zsssubrg  16536  cnsubrg  16538  gzrngunit  16543  zlpirlem1  16547  frgpcyg  16633  isphld  16664  css0  16695  pjfo  16721  unopn  16755  istps2OLD  16765  tsettps  16787  tgss2  16831  difopn  16877  incld  16886  iuncld  16888  indiscld  16934  mretopd  16935  resttop  16997  resttopon  16998  restfpw  17016  ordtbaslem  17024  ordtbas2  17027  ordtbas  17028  ordttopon  17029  ordtopn1  17030  ordtopn2  17031  ordtcld1  17033  ordtcld2  17034  ordtrest  17038  ordtrest2  17040  tgcn  17088  tgcnp  17089  cnpco  17102  cnt1  17184  cnrmnrm  17195  conndisj  17248  uncon  17261  2ndctop  17279  2ndcrest  17286  2ndcctbss  17287  2ndcomap  17290  dis2ndc  17292  restnlly  17314  islly2  17316  llyidm  17320  nllyidm  17321  dislly  17329  kgeni  17338  kgencmp2  17347  iskgen2  17349  kgencn2  17358  kgencn3  17359  elptr2  17375  ptbasfi  17382  txcld  17404  xkoccn  17419  txcn  17426  txdis  17432  txkgen  17452  xkopjcn  17456  xkococnlem  17459  cnmpt11  17463  cnmpt11f  17464  cnmpt1t  17465  cnmpt12  17467  cnmpt21  17471  cnmpt21f  17472  cnmpt2t  17473  cnmpt22  17474  cnmpt22f  17475  cnmpt1res  17476  cnmpt2res  17477  cnmptkp  17480  cnmptk1  17481  cnmpt1k  17482  cnmptkk  17483  cnmptk1p  17485  cnmptk2  17486  cnmpt2k  17488  txcon  17489  basqtop  17508  tgqtop  17509  qtopeu  17513  qtoprest  17514  qtopomap  17515  qtopcmap  17516  r0cld  17535  ordthmeolem  17598  pt1hmeo  17603  ptcmpfi  17610  xkocnv  17611  xkohmeo  17612  fbdmn0  17631  trfil1  17683  trfil2  17684  trfg  17688  uzrest  17694  uzfbas  17695  trufil  17707  elfm3  17747  rnelfm  17750  fmfnfmlem2  17752  fmfnfm  17755  txflf  17803  alexsublem  17840  alexsub  17841  alexsubb  17842  ptcmplem3  17850  ptcmplem4  17851  cnmpt1plusg  17872  cnmpt2plusg  17873  istgp2  17876  oppgtgp  17883  symgtgp  17886  subgtgp  17890  subgntr  17891  opnsubg  17892  cldsubg  17895  tgpconcomp  17897  tgpt0  17903  divstgplem  17905  divstgphaus  17907  prdstmdd  17908  tsms0  17926  tsmsadd  17931  tsmsxplem1  17937  tsmsxplem2  17938  cnmpt1vsca  17978  cnmpt2vsca  17979  xpsdsval  18047  xmeter  18081  mscl  18109  xmscl  18110  blcld  18153  stdbdxmet  18163  met2ndci  18170  ressxms  18173  ressms  18174  prdsxmslem2  18177  tmsxps  18184  tngngpd  18271  tngnrg  18287  sranlm  18297  lssnlm  18313  lssnvc  18314  xrsxmet  18417  xrsblre  18419  zdis  18424  icccmplem2  18431  xrge0tsms  18442  cnmpt1ds  18450  cnmpt2ds  18451  cncfmpt1f  18520  negcncf  18525  negfcncf  18526  cnheiborlem  18556  evth  18561  evth2  18562  lebnumlem1  18563  lebnumlem3  18565  xlebnum  18567  copco  18620  pcopt  18624  pcopt2  18625  pi1addf  18649  pi1addval  18650  pi1cof  18661  pi1coghm  18663  isclmi  18679  cphsubrglem  18717  cphreccllem  18718  cphcjcl  18723  cphsqrcl2  18726  cphsqrcl3  18727  cphqss  18728  cphnmf  18735  reipcl  18737  ipcau2  18768  cnmpt1ip  18778  cnmpt2ip  18779  clsocv  18781  iscauf  18810  cmetcaulem  18818  lmle  18831  lmcau  18842  lssbn  18877  hlprlem  18888  ishl2  18891  minveclem3b  18896  pjthlem2  18906  ovolfcl  18930  ovoliunlem1  18965  ovolshftlem1  18972  ovolicc2lem3  18982  ovolicc2lem4  18983  shftmbl  19000  inmbl  19003  difmbl  19004  volinun  19007  volfiniun  19008  voliunlem3  19013  volsup  19017  icombl1  19024  icombl  19025  ioombl  19026  iccmbl  19027  uniioombllem3  19044  uniioombllem5  19046  uniiccmbl  19049  dyaddisjlem  19054  dyadmbl  19059  opnmbllem  19060  volcn  19065  vitalilem1  19067  vitalilem4  19070  mbfdm  19087  mbfimasn  19093  mbfdm2  19097  mbfmulc2lem  19106  mbfmulc2re  19107  mbfneg  19109  mbfpos  19110  mbfposr  19111  mbfposb  19112  ismbf3d  19113  mbfimaopnlem  19114  cncombf  19117  mbfaddlem  19119  mbfadd  19120  mbfsub  19121  mbfmulc2  19122  mbflimsup  19125  mbflimlem  19126  i1fima  19137  i1fima2  19138  i1fima2sn  19139  i1fd  19140  i1f0rn  19141  itg11  19150  i1faddlem  19152  i1fadd  19154  i1fmul  19155  itg1addlem2  19156  itg1addlem4  19158  itg1addlem5  19159  itg1mulc  19163  i1fres  19164  i1fposd  19166  i1fsub  19167  itg1climres  19173  mbfi1fseqlem3  19176  mbfi1fseqlem4  19177  mbfi1fseqlem5  19178  mbfi1flimlem  19181  mbfi1flim  19182  mbfmullem2  19183  mbfmul  19185  itg2const  19199  itg2const2  19200  itg2seq  19201  itg2splitlem  19207  itg2monolem1  19209  itg2mono  19212  itg2gt0  19219  itg2cnlem1  19220  iblss  19263  i1fibl  19266  itgitg1  19267  itgss3  19273  ibladd  19279  iblsub  19280  iblabs  19287  bddmulibl  19297  bddibl  19298  cnmptlimc  19344  limccnp  19345  limccnp2  19346  limcco  19347  perfdvf  19357  dvcnp2  19373  cpnord  19388  cpncn  19389  cpnres  19390  dvcnvlem  19427  cmvth  19442  dvlip  19444  dvlipcn  19445  dvlip2  19446  c1liplem1  19447  c1lip1  19448  c1lip2  19449  dvgt0lem1  19453  lhop1lem  19464  lhop2  19466  lhop  19467  dvcnvrelem2  19469  dvcnvre  19470  dvfsumle  19472  dvfsumabs  19474  dvfsumlem2  19478  ftc1lem1  19486  ftc1lem2  19487  ftc1a  19488  ftc1lem4  19490  ftc2  19495  ftc2ditglem  19496  ftc2ditg  19497  itgsubstlem  19499  evlsval2  19508  mpfconst  19526  mpfproj  19527  mpfaddcl  19530  mpfmulcl  19531  pf1const  19533  pf1id  19534  pf1subrg  19535  mpfpf1  19538  pf1addcl  19540  pf1mulcl  19541  pf1ind  19542  tdeglem4  19550  deg1pwle  19609  deg1submon1p  19642  plyco0  19678  elplyd  19688  plypow  19691  plyconst  19692  plypf1  19698  plysub  19705  dgrcolem1  19758  dgrcolem2  19759  vieta1lem1  19794  vieta1lem2  19795  iaa  19809  aalioulem1  19816  aalioulem4  19819  aaliou3lem6  19832  tayl0  19845  taylpfval  19848  taylthlem2  19857  ulmdvlem1  19883  ulmdvlem3  19885  mtest  19887  mtestbdd  19888  mbfulm  19889  iblulm  19890  itgulm  19891  psercn2  19906  psercn  19909  abelthlem1  19914  abelthlem3  19916  abelth  19924  abelth2  19925  sincn  19927  coscn  19928  efcvx  19932  pige3  19992  cosne0  19999  tanregt0  20008  efif1olem4  20014  relogcl  20040  logdiv2  20079  logcn  20105  dvloglem  20106  logf1o2  20108  efopnlem2  20115  logccv  20121  cxpsqr  20161  loglesqr  20209  ang180lem1  20218  ang180lem2  20219  isosctrlem2  20230  angpined  20238  mcubic  20254  atanbnd  20333  atans2  20338  atantayl2  20345  atantayl3  20346  leibpi  20349  rlimcnp2  20372  efrlim  20375  cvxcl  20390  jensen  20394  emcllem6  20406  fsumharmonic  20417  ftalem2  20423  ftalem7  20428  basellem2  20431  basellem3  20432  basellem5  20434  basellem9  20438  ppiprm  20501  ppinprm  20502  chtprm  20503  chtnprm  20504  efchtdvds  20509  fsumdvdsmul  20547  chtublem  20562  fsumvma  20564  mersenne  20578  perfect  20582  dchrfi  20606  lgsne0  20684  lgseisenlem4  20703  lgsquadlem1  20705  2sqblem  20728  chebbnd2  20738  chto1lb  20739  rpvmasumlem  20748  dchrisumlem2  20751  dchrvmasumiflem1  20762  dchrvmasumiflem2  20763  dchrisum0fno1  20772  rpvmasum2  20773  dchrisum0re  20774  dchrisum0lem1  20777  dchrisum0lem2a  20778  dchrisum0lem2  20779  dchrisum0lem3  20780  dchrmusumlem  20783  dchrvmasumlem  20784  rpvmasum  20787  rplogsum  20788  mudivsum  20791  mulog2sumlem3  20797  2vmadivsumlem  20801  selberglem2  20807  selberg2lem  20811  logdivbnd  20817  selberg3lem1  20818  selberg4lem1  20821  selberg4  20822  pntrsumo1  20826  selberg3r  20830  selberg4r  20831  selberg34r  20832  pntrlog2bndlem4  20841  pntrlog2bndlem5  20842  pntrlog2bndlem6  20844  pntpbnd2  20848  pntlemo  20868  ablomul  21134  ghgrp  21147  rngoablo2  21201  vcoprne  21249  nvi  21284  ipval2lem3  21392  ipval2lem6  21398  ipf  21403  ubthlem1  21563  minvecolem2  21568  minvecolem4a  21570  hhshsslem2  21959  shsel1  22014  pjoccl  22126  5oalem1  22347  5oalem5  22351  3oalem2  22356  pjrni  22395  hmopd  22716  imaelshi  22752  adjbdlnb  22778  adjsslnop  22781  bracnlnval  22808  hmopidmchi  22845  disjabrex  23223  disjabrexf  23224  xrge0tsmsd  23415  lmxrge0  23493  trust  23533  tususp  23570  metustid  23598  indf1ofs  23689  esumf1o  23711  esumfsup  23726  esumpcvgval  23734  esumcvg  23742  unelsiga  23783  cldssbrsiga  23807  sxbrsigalem1  23899  ballotlemsf1o  24020  ballotlemrinv0  24039  eldmgm  24055  dmgmaddnn0  24060  lgamgulmlem2  24063  lgamcvg2  24088  regamcl  24094  relgamcl  24095  rpgamcl  24096  erdszelem8  24133  pconcon  24166  ptpcon  24168  txsconlem  24175  rescon  24181  cvmscld  24208  cvmliftmolem1  24216  cvmliftlem1  24220  cvmliftlem8  24227  cvmlift2lem9  24246  iseupa  24285  circum  24411  prodmolem2a  24561  fprodf1o  24573  fprodshft  24601  peano2dmgamma  24649  setlikespec  24745  wfrlem15  24828  onsuctop  25431  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  itgaddnclem2  25499  itgaddnc  25500  iblsubnc  25501  itgmulc2nclem2  25507  itgmulc2nc  25508  itgabsnc  25509  bddiblnc  25510  ftc1cnnclem  25513  areacirclem4  25519  isfne4  25593  islocfin  25620  neibastop1  25632  fnejoin2  25642  unirep  25673  sdclem2  25776  geomcau  25799  ssbnd  25835  prdsbnd2  25842  divrngcl  25911  1idl  25974  inidl  25978  prnc  26015  ispridlc  26018  elrfi  26092  mzpaddmpt  26142  mzpmulmpt  26143  diophun  26176  elpell1qr2  26280  pellfundglb  26293  qirropth  26316  rmspecfund  26317  rmbaserp  26327  rmxnn  26361  jm2.27a  26421  jm2.27c  26423  fnwe2lem3  26472  lnmfg  26503  kercvrlsm  26504  lnmepi  26506  pwssplit4  26514  frlmgsum  26555  uvcresum  26565  frlmsplit2  26566  frlmup1  26573  hbtlem5  26655  hbt  26657  rngunsnply  26701  symggen  26734  psgnunilem1  26739  psgnunilem3  26742  acsfn1p  26830  rfcnpre1  27013  refsumcn  27024  rfcnpre2  27025  refsum2cnlem1  27031  mulc1cncfg  27044  stoweidlem9  27081  stoweidlem17  27089  stoweidlem19  27091  stoweidlem20  27092  stoweidlem23  27095  stoweidlem31  27103  stoweidlem41  27113  stoweidlem47  27119  stirlinglem3  27148  stirlinglem7  27152  stirlinglem8  27153  stirlinglem11  27156  stirlinglem15  27160  sigardiv  27174  afvelrn  27356  bnj1145  28785  lkrlsp  29361  glbconN  29635  cvratlem  29679  llncvrlpln  29816  lplncvrlvol  29874  psubclsubN  30198  psubclinN  30206  4atexlemcnd  30330  cdleme23b  30608  cdlemk35  31170  dvaabl  31283  dia1elN  31313  diaintclN  31317  diasslssN  31318  dia2dimlem7  31329  dvadiaN  31387  dibintclN  31426  dihopelvalcpre  31507  dihsslss  31535  dih0rn  31543  dih1rn  31546  dihintcl  31603  dihmeetcl  31604  dochocss  31625  dochoccl  31628  dochsat  31642  dihsmsprn  31689  dochsnshp  31712  dochexmidlem6  31724  lcfl8b  31763  lclkrlem2g  31772  mapdpglem5N  31936  mapdpglem9  31939  mapdpglem14  31944  mapdpglem30a  31954  mapdpglem30b  31955  baerlem5amN  31975  baerlem5bmN  31976  baerlem5abmN  31977  mapdindp0  31978  mapdheq4lem  31990  mapdheq4  31991  mapdh6lem1N  31992  mapdh6lem2N  31993  mapdh7eN  32007  mapdh7cN  32008  mapdh7fN  32010  mapdh75e  32011  mapdh75fN  32014  mapdh8aa  32035  mapdh8d0N  32041  mapdh8d  32042  hdmap1eq2  32065  hdmap1eq4N  32066  hdmap1l6lem1  32067  hdmap1l6lem2  32068  hdmap1neglem1N  32087  hdmaprnlem7N  32117  hdmaprnlem17N  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2351  df-clel 2354
  Copyright terms: Public domain W3C validator