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

Theorem eqeltrrd 2508
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 2438 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2507 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  3eltr3d  2513  tz7.7  4732  fvmptdv2  5775  ffvresb  5861  xpexr2  6508  2ndrn  6611  1st2ndbr  6612  elopabi  6624  cnvf1olem  6659  dftpos4  6753  seqomlem4  6894  oneo  7008  oeordi  7014  oeeulem  7028  oeeui  7029  nnmordi  7058  nnneo  7078  th3qlem1  7194  disjen  7456  fnfi  7577  fsuppco  7639  elfi2  7652  fisupcl  7705  ordiso2  7717  ordtypelem9  7728  hartogslem2  7745  unxpwdom2  7791  noinfep  7853  cantnflt  7868  cantnfp1lem3  7876  cantnflem1  7885  cantnflem3  7887  cantnf  7889  cantnfltOLD  7898  cantnfp1lem3OLD  7902  cantnflem1OLD  7908  cantnflem3OLD  7909  cantnfOLD  7911  cnfcom3lem  7924  cnfcom3lemOLD  7932  r1pwss  7979  r0weon  8167  alephfp  8266  dfac2a  8287  cfsmolem  8427  enfin2i  8478  ac6num  8636  ttukeylem7  8672  fpwwe2lem9  8793  canthp1lem2  8808  pwfseqlem4  8817  gchaleph2  8827  wunun  8865  r1tskina  8937  tskun  8941  gruen  8967  subf  9600  resubcl  9661  negcon1ad  9702  subeq0bd  9762  rimul  10301  peano2nn  10322  nn0nnaddcl  10599  elnn0nn  10610  elz2  10651  zsubcl  10675  zrevaddcl  10678  zdiv  10700  peano5uzi  10718  peano2uzr  10898  uzaddcl  10899  qsubcl  10960  qrevaddcl  10963  xov1plusxeqvd  11418  fseq1p1m1  11518  om2uzrani  11759  uzrdglem  11764  seqf1olem2  11830  expaddzlem  11891  expaddz  11892  expmulz  11894  zesq  11971  bcm1k  12075  bccl  12082  permnn  12086  hashcl  12110  hashf1lem2  12193  hashf1  12194  seqcoll  12200  shftuz  12542  ref  12585  imf  12586  crre  12587  rereb  12593  absf  12809  lo1res2  13024  o1res2  13025  o1add2  13085  o1mul2  13086  o1sub2  13087  lo1sub  13092  isercoll2  13130  summolem2a  13176  fsumf1o  13184  fsumcnv  13224  fsumshft  13230  geolim2  13314  ruclem12  13506  sqr2irrlem  13513  oexpneg  13578  3dvds  13579  bitsf1  13625  gcdf  13686  sqnprm  13767  fnum  13803  fden  13804  phimullem  13837  pc2dvds  13928  gzsubcl  13984  4sqlem5  13986  4sqlem9  13990  4sqlem10  13991  mul4sqlem  13997  mul4sq  13998  4sqlem11  13999  4sqlem13  14001  4sqlem16  14004  4sqlem17  14005  4sqlem18  14006  vdwlem5  14029  vdwlem8  14032  vdwlem9  14033  ramub1lem2  14071  firest  14354  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  prdshom  14388  prdsbascl  14404  xpsaddlem  14496  xpsvsca  14500  xpsle  14502  mreincl  14520  ismred2  14524  mrcidb  14536  ssclem  14715  idffth  14826  ressffth  14831  coapm  14922  catciso  14958  evlfcl  15015  diag2cl  15039  hofcllem  15051  hofcl  15052  yonffthlem  15075  yoniso  15078  subsubm  15467  mhmima  15473  frmdss2  15521  mulgdir  15632  imasgrp2  15650  subgmulg  15675  issubg2  15676  issubgrpd2  15677  grpissubg  15681  subsubg  15684  cycsubgcl  15687  isnsg3  15695  ssnmz  15703  eqger  15711  ghmrn  15740  ghmnsgima  15750  conjsubg  15758  conjnmz  15760  subggim  15774  gass  15799  symggen  15956  psgnunilem1  15979  psgnunilem3  15982  mndodconglem  16024  odsubdvds  16050  sylow1lem1  16077  sylow1lem3  16079  sylow1lem4  16080  pgpssslw  16093  sylow2a  16098  sylow2blem3  16101  slwhash  16103  fislw  16104  sylow3lem2  16107  sylow3lem4  16109  sylow3lem5  16110  sylow3lem6  16111  lsmub1x  16125  lsmub2x  16126  lsmsubm  16132  lsmmod  16152  lsmdisj2  16159  subgdisj1  16168  efginvrel2  16204  efgsres  16215  efgsfo  16216  efgredleme  16220  iscygodd  16345  prmcyg  16350  gsumzsubmclOLD  16383  gsummptfsaddOLD  16395  gsum2d2lem  16439  pwsgsumOLD  16448  dprdcntz  16466  dprddisj  16467  dprdw  16468  dprdwOLD  16474  dprdfeq0  16486  dprdf11  16487  dprdfidOLD  16488  dprdfinvOLD  16490  dprdfaddOLD  16491  dprdfsubOLD  16492  dprdfeq0OLD  16493  dprdf11OLD  16494  dprdsubg  16495  dprdub  16496  dprdres  16499  dprdf1o  16503  dmdprdsplitlemOLD  16509  dprddisj2OLD  16512  dprd2dlem2  16513  dprd2dlem1  16514  dprd2da  16515  dmdprdsplit2  16519  dpjfval  16528  dpjidclOLD  16538  ablfacrplem  16540  ablfacrp  16541  ablfac1c  16546  ablfac1eu  16548  pgpfac1lem3a  16551  pgpfac1lem3  16552  pgpfaclem1  16556  pgpfaclem3  16558  ablfaclem3  16562  0unit  16706  irredneg  16736  irrednegb  16737  isdrng2  16766  subrgcrng  16793  subrgin  16812  subsubrg  16815  srngcl  16864  islmodd  16878  lssvancl1  16948  lss0cl  16950  lssvacl  16957  lssvscl  16958  lssvnegcl  16959  lssincl  16968  lmhmima  17050  lmhmrnlss  17053  lsslvec  17110  lspabs3  17124  lspdisj  17128  lspexch  17132  lsmcv  17144  lspsolv  17146  issubrngd2  17192  rlmlvec  17209  lidl1el  17222  drngnidl  17233  2idlcpbl  17238  isassad  17316  issubassa2  17337  psrass1lem  17381  mvridlemOLD  17426  mplsubrglem  17451  mplsubrglemOLD  17452  mplmonmul  17477  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  subrgasclcl  17513  mplmon2cl  17514  mplind  17516  zsssubrg  17715  cnsubrg  17717  gzrngunit  17722  zringlpirlem1  17745  zlpirlem1  17750  frgpcyg  17848  zrhpsgninv  17857  isphld  17925  css0  17956  pjfo  17982  frlmgsumOLD  18037  frlmsplit2  18039  frlmphllem  18047  frlmphl  18048  uvcresum  18060  mdetunilem6  18265  unopn  18358  istps2OLD  18368  tsettps  18390  tgss2  18434  difopn  18480  incld  18489  iuncld  18491  indiscld  18537  mretopd  18538  resttop  18606  resttopon  18607  restfpw  18625  ordtbaslem  18634  ordtbas2  18637  ordtbas  18638  ordttopon  18639  ordtopn1  18640  ordtopn2  18641  ordtcld1  18643  ordtcld2  18644  ordtrest  18648  ordtrest2  18650  tgcn  18698  tgcnp  18699  cnpco  18713  cnt1  18796  cnrmnrm  18807  conndisj  18862  uncon  18875  2ndctop  18893  2ndcrest  18900  2ndcctbss  18901  2ndcomap  18904  dis2ndc  18906  restnlly  18928  islly2  18930  llyidm  18934  nllyidm  18935  dislly  18943  kgeni  18952  kgencmp2  18961  iskgen2  18963  kgencn2  18972  kgencn3  18973  elptr2  18989  ptbasfi  18996  txcld  19018  xkoccn  19034  txcn  19041  txdis  19047  txkgen  19067  xkopjcn  19071  xkococnlem  19074  cnmpt11  19078  cnmpt11f  19079  cnmpt1t  19080  cnmpt12  19082  cnmpt21  19086  cnmpt21f  19087  cnmpt2t  19088  cnmpt22  19089  cnmpt22f  19090  cnmpt1res  19091  cnmptkp  19095  cnmptk1  19096  cnmpt1k  19097  cnmptkk  19098  cnmptk1p  19100  cnmptk2  19101  cnmpt2k  19103  txcon  19104  basqtop  19126  tgqtop  19127  qtopeu  19131  qtoprest  19132  qtopomap  19133  qtopcmap  19134  r0cld  19153  ordthmeolem  19216  pt1hmeo  19221  ptcmpfi  19228  xkocnv  19229  xkohmeo  19230  fbdmn0  19249  trfil1  19301  trfil2  19302  trfg  19306  uzrest  19312  uzfbas  19313  trufil  19325  elfm3  19365  rnelfm  19368  fmfnfmlem2  19370  fmfnfm  19373  txflf  19421  alexsublem  19458  alexsub  19459  alexsubb  19460  ptcmplem3  19468  ptcmplem4  19469  cnmpt1plusg  19500  cnmpt2plusg  19501  istgp2  19504  oppgtgp  19511  symgtgp  19514  subgtgp  19518  subgntr  19519  opnsubg  19520  cldsubg  19523  tgpconcomp  19525  tgpt0  19531  divstgplem  19533  divstgphaus  19535  prdstmdd  19536  tsms0  19557  tsmsadd  19563  tsmsxplem1  19569  tsmsxplem2  19570  cnmpt1vsca  19610  cnmpt2vsca  19611  trust  19646  uspreg  19691  xpsdsval  19798  xmeter  19850  mscl  19878  xmscl  19879  blcld  19922  stdbdxmet  19932  met2ndci  19939  prdsxmslem2  19946  tmsxps  19953  metustidOLD  19976  metustid  19977  tngngpd  20081  tngnrg  20097  sranlm  20107  lssnlm  20123  lssnvc  20124  xrsxmet  20228  xrsblre  20230  zdis  20235  icccmplem2  20242  xrge0tsms  20253  cnmpt1ds  20261  cnmpt2ds  20262  cncfmpt1f  20331  negcncf  20336  negfcncf  20337  cnheiborlem  20368  evth  20373  evth2  20374  lebnumlem1  20375  lebnumlem3  20377  xlebnum  20379  copco  20432  pcopt  20436  pcopt2  20437  pi1addf  20461  pi1addval  20462  pi1cof  20473  pi1coghm  20475  isclmi  20491  cphsubrglem  20538  cphreccllem  20539  cphcjcl  20544  cphsqrcl2  20547  cphsqrcl3  20548  cphqss  20549  cphnmf  20556  reipcl  20558  ipcau2  20591  cnmpt1ip  20601  cnmpt2ip  20602  clsocv  20604  iscauf  20633  cmetcaulem  20641  lmle  20654  lmcau  20665  lssbn  20704  hlprlem  20721  ishl2  20724  minveclem3b  20757  pjthlem2  20767  ovolfcl  20792  ovoliunlem1  20827  ovolshftlem1  20834  ovolicc2lem3  20844  ovolicc2lem4  20845  shftmbl  20862  inmbl  20865  difmbl  20866  volinun  20869  volfiniun  20870  voliunlem3  20875  volsup  20879  icombl1  20886  icombl  20887  ioombl  20888  iccmbl  20889  uniioombllem3  20907  uniioombllem5  20909  uniiccmbl  20912  dyaddisjlem  20917  dyadmbl  20922  opnmbllem  20923  volcn  20928  vitalilem1  20930  vitalilem4  20933  mbfdm  20948  mbfimasn  20954  mbfdm2  20958  mbfmulc2lem  20967  mbfmulc2re  20968  mbfneg  20970  mbfpos  20971  mbfposr  20972  mbfposb  20973  ismbf3d  20974  mbfimaopnlem  20975  cncombf  20978  mbfaddlem  20980  mbfadd  20981  mbfsub  20982  mbfmulc2  20983  mbflimsup  20986  mbflimlem  20987  i1fima  20998  i1fima2  20999  i1fima2sn  21000  i1fd  21001  i1f0rn  21002  itg11  21011  i1faddlem  21013  i1fadd  21015  i1fmul  21016  itg1addlem2  21017  itg1addlem4  21019  itg1addlem5  21020  itg1mulc  21024  i1fres  21025  i1fposd  21027  i1fsub  21028  itg1climres  21034  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1flimlem  21042  mbfi1flim  21043  mbfmullem2  21044  mbfmul  21046  itg2const  21060  itg2const2  21061  itg2seq  21062  itg2splitlem  21068  itg2monolem1  21070  itg2mono  21073  itg2gt0  21080  itg2cnlem1  21081  iblss  21124  i1fibl  21127  itgitg1  21128  itgss3  21134  ibladd  21140  iblsub  21141  iblabs  21148  bddmulibl  21158  bddibl  21159  cnmptlimc  21207  limccnp  21208  limccnp2  21209  perfdvf  21220  dvcnp2  21236  cpnord  21251  cpncn  21252  cpnres  21253  dvcnvlem  21290  cmvth  21305  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  c1lip1  21311  c1lip2  21312  dvgt0lem1  21316  lhop1lem  21327  lhop2  21329  lhop  21330  dvcnvrelem2  21332  dvcnvre  21333  dvfsumle  21335  dvfsumabs  21337  dvfsumlem2  21341  ftc1lem1  21349  ftc1lem2  21350  ftc1a  21351  ftc1lem4  21353  ftc2  21358  ftc2ditglem  21359  ftc2ditg  21360  itgsubstlem  21362  evlsval2  21372  mpfconst  21390  mpfproj  21391  mpfaddcl  21394  mpfmulcl  21395  pf1const  21397  pf1id  21398  pf1subrg  21399  mpfpf1  21402  pf1addcl  21404  pf1mulcl  21405  pf1ind  21406  deg1pwle  21476  deg1submon1p  21509  plyco0  21545  elplyd  21555  plypow  21558  plyconst  21559  plypf1  21565  plysub  21572  dgrcolem1  21625  dgrcolem2  21626  vieta1lem1  21661  vieta1lem2  21662  iaa  21676  aalioulem1  21683  aalioulem4  21686  aaliou3lem6  21699  tayl0  21712  taylpfval  21715  taylthlem2  21724  ulmdvlem1  21750  ulmdvlem3  21752  mtest  21754  mtestbdd  21755  mbfulm  21756  iblulm  21757  itgulm  21758  psercn2  21773  psercn  21776  abelthlem1  21781  abelthlem3  21783  abelth  21791  abelth2  21792  sincn  21794  coscn  21795  efcvx  21799  pige3  21864  cosne0  21871  tanregt0  21880  efif1olem4  21886  relogcl  21912  logdiv2  21951  logcn  21977  dvloglem  21978  logf1o2  21980  efopnlem2  21987  logccv  21993  cxpsqr  22033  loglesqr  22081  ang180lem1  22090  ang180lem2  22091  isosctrlem2  22102  angpined  22110  mcubic  22127  atanbnd  22206  atans2  22211  atantayl2  22218  atantayl3  22219  leibpi  22222  rlimcnp2  22245  efrlim  22248  cvxcl  22263  emcllem6  22279  fsumharmonic  22290  ftalem2  22296  ftalem7  22301  basellem2  22304  basellem3  22305  basellem5  22307  basellem9  22311  ppiprm  22374  ppinprm  22375  chtprm  22376  chtnprm  22377  efchtdvds  22382  fsumdvdsmul  22420  chtublem  22435  fsumvma  22437  mersenne  22451  perfect  22455  dchrfi  22479  lgsne0  22557  lgseisenlem4  22576  lgsquadlem1  22578  2sqblem  22601  chebbnd2  22611  chto1lb  22612  rpvmasumlem  22621  dchrisumlem2  22624  dchrvmasumiflem1  22635  dchrvmasumiflem2  22636  dchrisum0fno1  22645  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  dchrmusumlem  22656  dchrvmasumlem  22657  rpvmasum  22660  rplogsum  22661  mudivsum  22664  mulog2sumlem3  22670  2vmadivsumlem  22674  selberglem2  22680  selberg2lem  22684  logdivbnd  22690  selberg3lem1  22691  selberg4lem1  22694  selberg4  22695  pntrsumo1  22699  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntpbnd2  22721  pntlemo  22741  tgbtwnexch2  22831  tgbtwnxfr  22860  tghilbert1_1  22914  colline  22918  mirreu3  22924  ttgcontlem1  22954  iseupa  23409  ablomul  23665  ghgrp  23678  rngoablo2  23732  vcoprne  23780  nvi  23815  ipval2lem3  23923  ipval2lem6  23929  ipf  23934  ubthlem1  24094  minvecolem2  24099  minvecolem4a  24101  hhshsslem2  24492  shsel1  24547  pjoccl  24659  5oalem1  24880  5oalem5  24884  3oalem2  24889  pjrni  24928  hmopd  25249  imaelshi  25285  adjbdlnb  25311  adjsslnop  25314  bracnlnval  25341  hmopidmchi  25378  disjabrex  25750  disjabrexf  25751  fgreu  25814  fpwrelmapffslem  25857  archiabllem2c  26036  xrge0tsmsd  26106  suborng  26136  metideq  26174  ordtrestNEW  26205  ordtrest2NEW  26207  lmxrge0  26236  indf1ofs  26336  esumf1o  26358  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  unelsiga  26431  cldssbrsiga  26455  sxbrsigalem1  26554  eulerpartlemsf  26590  eulerpartlems  26591  eulerpartlemb  26599  eulerpartgbij  26603  eulerpartlemgh  26609  fibp1  26632  ballotlemsf1o  26744  ballotlemrinv0  26763  sgnmulsgp  26781  plyrecld  26798  signslema  26811  signsvtn0  26819  signstfveq0  26826  eldmgm  26856  dmgmaddnn0  26861  lgamgulmlem2  26864  lgamcvg2  26889  regamcl  26895  relgamcl  26896  rpgamcl  26897  erdszelem8  26934  pconcon  26968  ptpcon  26970  txsconlem  26977  rescon  26983  cvmscld  27010  cvmliftmolem1  27018  cvmliftlem1  27022  cvmliftlem8  27029  cvmlift2lem9  27048  circum  27166  prodmolem2a  27294  fprodf1o  27306  fprodshft  27334  setlikespec  27495  wfrlem15  27585  onsuctop  28127  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  mbfresfi  28282  mbfposadd  28283  itg2addnclem  28287  itg2addnclem2  28288  itg2addnc  28290  itgaddnclem2  28295  itgaddnc  28296  iblsubnc  28297  itgmulc2nclem2  28303  itgmulc2nc  28304  itgabsnc  28305  bddiblnc  28306  ftc1cnnclem  28309  ftc1anclem1  28311  ftc1anclem2  28312  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ftc2nc  28320  areacirclem2  28329  isfne4  28385  islocfin  28412  fnejoin2  28434  sdclem2  28482  geomcau  28499  ssbnd  28531  prdsbnd2  28538  divrngcl  28607  1idl  28670  inidl  28674  prnc  28711  ispridlc  28714  elrfi  28875  mzpaddmpt  28922  mzpmulmpt  28923  diophun  28957  elpell1qr2  29058  pellfundglb  29071  qirropth  29094  rmspecfund  29095  rmbaserp  29105  rmxnn  29139  jm2.27a  29199  jm2.27c  29201  fnwe2lem3  29250  lnmfg  29280  kercvrlsm  29281  lnmepi  29283  pwssplit4  29287  hbtlem5  29329  hbt  29331  rngunsnply  29375  acsfn1p  29401  iocmbl  29433  itgpowd  29435  rfcnpre1  29586  refsumcn  29597  rfcnpre2  29598  rfcnpre3  29600  rfcnpre4  29601  refsum2cnlem1  29604  mulc1cncfg  29616  stoweidlem9  29650  stoweidlem17  29658  stoweidlem19  29660  stoweidlem20  29661  stoweidlem23  29664  stoweidlem31  29672  stoweidlem41  29682  stoweidlem47  29688  stirlinglem3  29717  stirlinglem7  29721  stirlinglem8  29722  sigardiv  29743  afvelrn  29920  edgwlk  30140  extwwlkfablem1  30513  numclwlk2lem2f1o  30544  bnj1145  31686  riotasvd  32180  lkrlsp  32320  glbconN  32594  cvratlem  32638  llncvrlpln  32775  lplncvrlvol  32833  psubclsubN  33157  psubclinN  33165  4atexlemcnd  33289  cdleme23b  33567  cdlemk35  34129  dvaabl  34242  dia1elN  34272  diaintclN  34276  diasslssN  34277  dia2dimlem7  34288  dvadiaN  34346  dibintclN  34385  dihopelvalcpre  34466  dihsslss  34494  dih0rn  34502  dih1rn  34505  dihintcl  34562  dihmeetcl  34563  dochocss  34584  dochoccl  34587  dochsat  34601  dihsmsprn  34648  dochsnshp  34671  dochexmidlem6  34683  lcfl8b  34722  lclkrlem2g  34731  mapdpglem5N  34895  mapdpglem9  34898  mapdpglem14  34903  mapdpglem30a  34913  mapdpglem30b  34914  baerlem5amN  34934  baerlem5bmN  34935  baerlem5abmN  34936  mapdindp0  34937  mapdheq4lem  34949  mapdheq4  34950  mapdh6lem1N  34951  mapdh6lem2N  34952  mapdh7eN  34966  mapdh7cN  34967  mapdh7fN  34969  mapdh75e  34970  mapdh75fN  34973  mapdh8aa  34994  mapdh8d0N  35000  mapdh8d  35001  hdmap1eq2  35024  hdmap1eq4N  35025  hdmap1l6lem1  35026  hdmap1l6lem2  35027  hdmap1neglem1N  35046  hdmaprnlem7N  35076  hdmaprnlem17N  35084
  Copyright terms: Public domain W3C validator