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

Theorem eqeltrrd 2513
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 2443 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2512 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  3eltr3d  2518  tz7.7  4740  fvmptdv2  5782  ffvresb  5869  xpexr2  6514  2ndrn  6617  1st2ndbr  6618  elopabi  6630  cnvf1olem  6665  dftpos4  6759  seqomlem4  6900  oneo  7012  oeordi  7018  oeeulem  7032  oeeui  7033  nnmordi  7062  nnneo  7082  th3qlem1  7198  disjen  7460  fnfi  7581  fsuppco  7643  elfi2  7656  fisupcl  7709  ordiso2  7721  ordtypelem9  7732  hartogslem2  7749  unxpwdom2  7795  noinfep  7857  cantnflt  7872  cantnfp1lem3  7880  cantnflem1  7889  cantnflem3  7891  cantnf  7893  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnflem1OLD  7912  cantnflem3OLD  7913  cantnfOLD  7915  cnfcom3lem  7928  cnfcom3lemOLD  7936  r1pwss  7983  r0weon  8171  alephfp  8270  dfac2a  8291  cfsmolem  8431  enfin2i  8482  ac6num  8640  ttukeylem7  8676  fpwwe2lem9  8797  canthp1lem2  8812  pwfseqlem4  8821  gchaleph2  8831  wunun  8869  r1tskina  8941  tskun  8945  gruen  8971  subf  9604  resubcl  9665  negcon1ad  9706  subeq0bd  9766  rimul  10305  peano2nn  10326  nn0nnaddcl  10603  elnn0nn  10614  elz2  10655  zsubcl  10679  zrevaddcl  10682  zdiv  10704  peano5uzi  10722  peano2uzr  10902  uzaddcl  10903  qsubcl  10964  qrevaddcl  10967  xov1plusxeqvd  11423  fseq1p1m1  11526  om2uzrani  11767  uzrdglem  11772  seqf1olem2  11838  expaddzlem  11899  expaddz  11900  expmulz  11902  zesq  11979  bcm1k  12083  bccl  12090  permnn  12094  hashcl  12118  hashf1lem2  12201  hashf1  12202  seqcoll  12208  shftuz  12550  ref  12593  imf  12594  crre  12595  rereb  12601  absf  12817  lo1res2  13032  o1res2  13033  o1add2  13093  o1mul2  13094  o1sub2  13095  lo1sub  13100  isercoll2  13138  summolem2a  13184  fsumf1o  13192  fsumcnv  13232  mptfzshft  13237  geolim2  13323  ruclem12  13515  sqr2irrlem  13522  oexpneg  13587  3dvds  13588  bitsf1  13634  gcdf  13695  sqnprm  13776  fnum  13812  fden  13813  phimullem  13846  pc2dvds  13937  gzsubcl  13993  4sqlem5  13995  4sqlem9  13999  4sqlem10  14000  mul4sqlem  14006  mul4sq  14007  4sqlem11  14008  4sqlem13  14010  4sqlem16  14013  4sqlem17  14014  4sqlem18  14015  vdwlem5  14038  vdwlem8  14041  vdwlem9  14042  ramub1lem2  14080  firest  14363  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdshom  14397  prdsbascl  14413  xpsaddlem  14505  xpsvsca  14509  xpsle  14511  mreincl  14529  ismred2  14533  mrcidb  14545  ssclem  14724  idffth  14835  ressffth  14840  coapm  14931  catciso  14967  evlfcl  15024  diag2cl  15048  hofcllem  15060  hofcl  15061  yonffthlem  15084  yoniso  15087  subsubm  15476  mhmima  15482  frmdss2  15532  mulgdir  15643  imasgrp2  15661  subgmulg  15686  issubg2  15687  issubgrpd2  15688  grpissubg  15692  subsubg  15695  cycsubgcl  15698  isnsg3  15706  ssnmz  15714  eqger  15722  ghmrn  15751  ghmnsgima  15761  conjsubg  15769  conjnmz  15771  subggim  15785  gass  15810  symggen  15967  psgnunilem1  15990  psgnunilem3  15993  mndodconglem  16035  odsubdvds  16061  sylow1lem1  16088  sylow1lem3  16090  sylow1lem4  16091  pgpssslw  16104  sylow2a  16109  sylow2blem3  16112  slwhash  16114  fislw  16115  sylow3lem2  16118  sylow3lem4  16120  sylow3lem5  16121  sylow3lem6  16122  lsmub1x  16136  lsmub2x  16137  lsmsubm  16143  lsmmod  16163  lsmdisj2  16170  subgdisj1  16179  efginvrel2  16215  efgsres  16226  efgsfo  16227  efgredleme  16231  iscygodd  16356  prmcyg  16361  gsumzsubmclOLD  16394  gsummptfsaddOLD  16406  gsum2d2lem  16453  pwsgsumOLD  16462  dprdcntz  16480  dprddisj  16481  dprdw  16482  dprdwOLD  16488  dprdfeq0  16500  dprdf11  16501  dprdfidOLD  16502  dprdfinvOLD  16504  dprdfaddOLD  16505  dprdfsubOLD  16506  dprdfeq0OLD  16507  dprdf11OLD  16508  dprdsubg  16509  dprdub  16510  dprdres  16513  dprdf1o  16517  dmdprdsplitlemOLD  16523  dprddisj2OLD  16526  dprd2dlem2  16527  dprd2dlem1  16528  dprd2da  16529  dmdprdsplit2  16533  dpjfval  16542  dpjidclOLD  16552  ablfacrplem  16554  ablfacrp  16555  ablfac1c  16560  ablfac1eu  16562  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfaclem1  16570  pgpfaclem3  16572  ablfaclem3  16576  0unit  16760  irredneg  16790  irrednegb  16791  isdrng2  16820  subrgcrng  16847  subrgin  16866  subsubrg  16869  srngcl  16918  islmodd  16932  lssvancl1  17003  lss0cl  17005  lssvacl  17012  lssvscl  17013  lssvnegcl  17014  lssincl  17023  lmhmima  17105  lmhmrnlss  17108  lsslvec  17165  lspabs3  17179  lspdisj  17183  lspexch  17187  lsmcv  17199  lspsolv  17201  issubrngd2  17247  rlmlvec  17264  lidl1el  17277  drngnidl  17288  2idlcpbl  17293  isassad  17371  issubassa2  17392  psrass1lem  17424  mvridlemOLD  17469  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  subrgasclcl  17556  mplmon2cl  17557  mplind  17559  evlsval2  17581  mpfconst  17591  mpfproj  17592  mpfaddcl  17595  mpfmulcl  17596  pf1const  17755  pf1id  17756  pf1subrg  17757  mpfpf1  17760  pf1addcl  17762  pf1mulcl  17763  pf1ind  17764  zsssubrg  17846  cnsubrg  17848  gzrngunit  17853  zringlpirlem1  17878  zlpirlem1  17883  frgpcyg  17981  zrhpsgninv  17990  isphld  18058  css0  18089  pjfo  18115  frlmgsumOLD  18170  frlmsplit2  18172  frlmphllem  18180  frlmphl  18181  uvcresum  18193  mdetunilem6  18398  unopn  18491  istps2OLD  18501  tsettps  18523  tgss2  18567  difopn  18613  incld  18622  iuncld  18624  indiscld  18670  mretopd  18671  resttop  18739  resttopon  18740  restfpw  18758  ordtbaslem  18767  ordtbas2  18770  ordtbas  18771  ordttopon  18772  ordtopn1  18773  ordtopn2  18774  ordtcld1  18776  ordtcld2  18777  ordtrest  18781  ordtrest2  18783  tgcn  18831  tgcnp  18832  cnpco  18846  cnt1  18929  cnrmnrm  18940  conndisj  18995  uncon  19008  2ndctop  19026  2ndcrest  19033  2ndcctbss  19034  2ndcomap  19037  dis2ndc  19039  restnlly  19061  islly2  19063  llyidm  19067  nllyidm  19068  dislly  19076  kgeni  19085  kgencmp2  19094  iskgen2  19096  kgencn2  19105  kgencn3  19106  elptr2  19122  ptbasfi  19129  txcld  19151  xkoccn  19167  txcn  19174  txdis  19180  txkgen  19200  xkopjcn  19204  xkococnlem  19207  cnmpt11  19211  cnmpt11f  19212  cnmpt1t  19213  cnmpt12  19215  cnmpt21  19219  cnmpt21f  19220  cnmpt2t  19221  cnmpt22  19222  cnmpt22f  19223  cnmpt1res  19224  cnmptkp  19228  cnmptk1  19229  cnmpt1k  19230  cnmptkk  19231  cnmptk1p  19233  cnmptk2  19234  cnmpt2k  19236  txcon  19237  basqtop  19259  tgqtop  19260  qtopeu  19264  qtoprest  19265  qtopomap  19266  qtopcmap  19267  r0cld  19286  ordthmeolem  19349  pt1hmeo  19354  ptcmpfi  19361  xkocnv  19362  xkohmeo  19363  fbdmn0  19382  trfil1  19434  trfil2  19435  trfg  19439  uzrest  19445  uzfbas  19446  trufil  19458  elfm3  19498  rnelfm  19501  fmfnfmlem2  19503  fmfnfm  19506  txflf  19554  alexsublem  19591  alexsub  19592  alexsubb  19593  ptcmplem3  19601  ptcmplem4  19602  cnmpt1plusg  19633  cnmpt2plusg  19634  istgp2  19637  oppgtgp  19644  symgtgp  19647  subgtgp  19651  subgntr  19652  opnsubg  19653  cldsubg  19656  tgpconcomp  19658  tgpt0  19664  divstgplem  19666  divstgphaus  19668  prdstmdd  19669  tsms0  19690  tsmsadd  19696  tsmsxplem1  19702  tsmsxplem2  19703  cnmpt1vsca  19743  cnmpt2vsca  19744  trust  19779  uspreg  19824  xpsdsval  19931  xmeter  19983  mscl  20011  xmscl  20012  blcld  20055  stdbdxmet  20065  met2ndci  20072  prdsxmslem2  20079  tmsxps  20086  metustidOLD  20109  metustid  20110  tngngpd  20214  tngnrg  20230  sranlm  20240  lssnlm  20256  lssnvc  20257  xrsxmet  20361  xrsblre  20363  zdis  20368  icccmplem2  20375  xrge0tsms  20386  cnmpt1ds  20394  cnmpt2ds  20395  cncfmpt1f  20464  negcncf  20469  negfcncf  20470  cnheiborlem  20501  evth  20506  evth2  20507  lebnumlem1  20508  lebnumlem3  20510  xlebnum  20512  copco  20565  pcopt  20569  pcopt2  20570  pi1addf  20594  pi1addval  20595  pi1cof  20606  pi1coghm  20608  isclmi  20624  cphsubrglem  20671  cphreccllem  20672  cphcjcl  20677  cphsqrcl2  20680  cphsqrcl3  20681  cphqss  20682  cphnmf  20689  reipcl  20691  ipcau2  20724  cnmpt1ip  20734  cnmpt2ip  20735  clsocv  20737  iscauf  20766  cmetcaulem  20774  lmle  20787  lmcau  20798  lssbn  20837  hlprlem  20854  ishl2  20857  minveclem3b  20890  pjthlem2  20900  ovolfcl  20925  ovoliunlem1  20960  ovolshftlem1  20967  ovolicc2lem3  20977  ovolicc2lem4  20978  shftmbl  20995  inmbl  20998  difmbl  20999  volinun  21002  volfiniun  21003  voliunlem3  21008  volsup  21012  icombl1  21019  icombl  21020  ioombl  21021  iccmbl  21022  uniioombllem3  21040  uniioombllem5  21042  uniiccmbl  21045  dyaddisjlem  21050  dyadmbl  21055  opnmbllem  21056  volcn  21061  vitalilem1  21063  vitalilem4  21066  mbfdm  21081  mbfimasn  21087  mbfdm2  21091  mbfmulc2lem  21100  mbfmulc2re  21101  mbfneg  21103  mbfpos  21104  mbfposr  21105  mbfposb  21106  ismbf3d  21107  mbfimaopnlem  21108  cncombf  21111  mbfaddlem  21113  mbfadd  21114  mbfsub  21115  mbfmulc2  21116  mbflimsup  21119  mbflimlem  21120  i1fima  21131  i1fima2  21132  i1fima2sn  21133  i1fd  21134  i1f0rn  21135  itg11  21144  i1faddlem  21146  i1fadd  21148  i1fmul  21149  itg1addlem2  21150  itg1addlem4  21152  itg1addlem5  21153  itg1mulc  21157  i1fres  21158  i1fposd  21160  i1fsub  21161  itg1climres  21167  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1flimlem  21175  mbfi1flim  21176  mbfmullem2  21177  mbfmul  21179  itg2const  21193  itg2const2  21194  itg2seq  21195  itg2splitlem  21201  itg2monolem1  21203  itg2mono  21206  itg2gt0  21213  itg2cnlem1  21214  iblss  21257  i1fibl  21260  itgitg1  21261  itgss3  21267  ibladd  21273  iblsub  21274  iblabs  21281  bddmulibl  21291  bddibl  21292  cnmptlimc  21340  limccnp  21341  limccnp2  21342  perfdvf  21353  dvcnp2  21369  cpnord  21384  cpncn  21385  cpnres  21386  dvcnvlem  21423  cmvth  21438  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  c1lip1  21444  c1lip2  21445  dvgt0lem1  21449  lhop1lem  21460  lhop2  21462  lhop  21463  dvcnvrelem2  21465  dvcnvre  21466  dvfsumle  21468  dvfsumabs  21470  dvfsumlem2  21474  ftc1lem1  21482  ftc1lem2  21483  ftc1a  21484  ftc1lem4  21486  ftc2  21491  ftc2ditglem  21492  ftc2ditg  21493  itgsubstlem  21495  deg1pwle  21566  deg1submon1p  21599  plyco0  21635  elplyd  21645  plypow  21648  plyconst  21649  plypf1  21655  plysub  21662  dgrcolem1  21715  dgrcolem2  21716  vieta1lem1  21751  vieta1lem2  21752  iaa  21766  aalioulem1  21773  aalioulem4  21776  aaliou3lem6  21789  tayl0  21802  taylpfval  21805  taylthlem2  21814  ulmdvlem1  21840  ulmdvlem3  21842  mtest  21844  mtestbdd  21845  mbfulm  21846  iblulm  21847  itgulm  21848  psercn2  21863  psercn  21866  abelthlem1  21871  abelthlem3  21873  abelth  21881  abelth2  21882  sincn  21884  coscn  21885  efcvx  21889  pige3  21954  cosne0  21961  tanregt0  21970  efif1olem4  21976  relogcl  22002  logdiv2  22041  logcn  22067  dvloglem  22068  logf1o2  22070  efopnlem2  22077  logccv  22083  cxpsqr  22123  loglesqr  22171  ang180lem1  22180  ang180lem2  22181  isosctrlem2  22192  angpined  22200  mcubic  22217  atanbnd  22296  atans2  22301  atantayl2  22308  atantayl3  22309  leibpi  22312  rlimcnp2  22335  efrlim  22338  cvxcl  22353  emcllem6  22369  fsumharmonic  22380  ftalem2  22386  ftalem7  22391  basellem2  22394  basellem3  22395  basellem5  22397  basellem9  22401  ppiprm  22464  ppinprm  22465  chtprm  22466  chtnprm  22467  efchtdvds  22472  fsumdvdsmul  22510  chtublem  22525  fsumvma  22527  mersenne  22541  perfect  22545  dchrfi  22569  lgsne0  22647  lgseisenlem4  22666  lgsquadlem1  22668  2sqblem  22691  chebbnd2  22701  chto1lb  22702  rpvmasumlem  22711  dchrisumlem2  22714  dchrvmasumiflem1  22725  dchrvmasumiflem2  22726  dchrisum0fno1  22735  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  dchrmusumlem  22746  dchrvmasumlem  22747  rpvmasum  22750  rplogsum  22751  mudivsum  22754  mulog2sumlem3  22760  2vmadivsumlem  22764  selberglem2  22770  selberg2lem  22774  logdivbnd  22780  selberg3lem1  22781  selberg4lem1  22784  selberg4  22785  pntrsumo1  22789  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntpbnd2  22811  pntlemo  22831  tgbtwnexch2  22924  tgbtwnxfr  22954  tghilbert1_1  23013  colline  23020  mirreu3  23026  ttgcontlem1  23082  iseupa  23537  ablomul  23793  ghgrp  23806  rngoablo2  23860  vcoprne  23908  nvi  23943  ipval2lem3  24051  ipval2lem6  24057  ipf  24062  ubthlem1  24222  minvecolem2  24227  minvecolem4a  24229  hhshsslem2  24620  shsel1  24675  pjoccl  24787  5oalem1  25008  5oalem5  25012  3oalem2  25017  pjrni  25056  hmopd  25377  imaelshi  25413  adjbdlnb  25439  adjsslnop  25442  bracnlnval  25469  hmopidmchi  25506  disjabrex  25877  disjabrexf  25878  fgreu  25941  ffsrn  25980  fpwrelmapffslem  25983  archiabllem2c  26163  xrge0tsmsd  26204  suborng  26234  metideq  26272  ordtrestNEW  26303  ordtrest2NEW  26305  lmxrge0  26334  indf1ofs  26434  esumf1o  26456  esumfsup  26471  esumpcvgval  26479  esumcvg  26487  unelsiga  26529  cldssbrsiga  26553  sxbrsigalem1  26652  eulerpartlemsf  26694  eulerpartlems  26695  eulerpartlemb  26703  eulerpartgbij  26707  eulerpartlemgh  26713  fibp1  26736  ballotlemsf1o  26848  ballotlemrinv0  26867  sgnmulsgp  26885  plyrecld  26902  signslema  26915  signsvtn0  26923  signstfveq0  26930  eldmgm  26960  dmgmaddnn0  26965  lgamgulmlem2  26968  lgamcvg2  26993  regamcl  26999  relgamcl  27000  rpgamcl  27001  erdszelem8  27038  pconcon  27072  ptpcon  27074  txsconlem  27081  rescon  27087  cvmscld  27114  cvmliftmolem1  27122  cvmliftlem1  27126  cvmliftlem8  27133  cvmlift2lem9  27152  circum  27270  prodmolem2a  27398  fprodf1o  27410  fprodshft  27438  setlikespec  27599  wfrlem15  27689  onsuctop  28231  mblfinlem1  28381  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  mbfresfi  28391  mbfposadd  28392  itg2addnclem  28396  itg2addnclem2  28397  itg2addnc  28399  itgaddnclem2  28404  itgaddnc  28405  iblsubnc  28406  itgmulc2nclem2  28412  itgmulc2nc  28413  itgabsnc  28414  bddiblnc  28415  ftc1cnnclem  28418  ftc1anclem1  28420  ftc1anclem2  28421  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ftc2nc  28429  areacirclem2  28438  isfne4  28494  islocfin  28521  fnejoin2  28543  sdclem2  28591  geomcau  28608  ssbnd  28640  prdsbnd2  28647  divrngcl  28716  1idl  28779  inidl  28783  prnc  28820  ispridlc  28823  elrfi  28983  mzpaddmpt  29030  mzpmulmpt  29031  diophun  29065  elpell1qr2  29166  pellfundglb  29179  qirropth  29202  rmspecfund  29203  rmbaserp  29213  rmxnn  29247  jm2.27a  29307  jm2.27c  29309  fnwe2lem3  29358  lnmfg  29388  kercvrlsm  29389  lnmepi  29391  pwssplit4  29395  hbtlem5  29437  hbt  29439  rngunsnply  29483  acsfn1p  29509  iocmbl  29541  itgpowd  29543  rfcnpre1  29694  refsumcn  29705  rfcnpre2  29706  rfcnpre3  29708  rfcnpre4  29709  refsum2cnlem1  29712  mulc1cncfg  29723  stoweidlem9  29757  stoweidlem17  29765  stoweidlem19  29767  stoweidlem20  29768  stoweidlem23  29771  stoweidlem31  29779  stoweidlem41  29789  stoweidlem47  29795  stirlinglem3  29824  stirlinglem7  29828  stirlinglem8  29829  sigardiv  29850  afvelrn  30027  edgwlk  30247  extwwlkfablem1  30620  numclwlk2lem2f1o  30651  bnj1145  31871  riotasvd  32447  lkrlsp  32587  glbconN  32861  cvratlem  32905  llncvrlpln  33042  lplncvrlvol  33100  psubclsubN  33424  psubclinN  33432  4atexlemcnd  33556  cdleme23b  33834  cdlemk35  34396  dvaabl  34509  dia1elN  34539  diaintclN  34543  diasslssN  34544  dia2dimlem7  34555  dvadiaN  34613  dibintclN  34652  dihopelvalcpre  34733  dihsslss  34761  dih0rn  34769  dih1rn  34772  dihintcl  34829  dihmeetcl  34830  dochocss  34851  dochoccl  34854  dochsat  34868  dihsmsprn  34915  dochsnshp  34938  dochexmidlem6  34950  lcfl8b  34989  lclkrlem2g  34998  mapdpglem5N  35162  mapdpglem9  35165  mapdpglem14  35170  mapdpglem30a  35180  mapdpglem30b  35181  baerlem5amN  35201  baerlem5bmN  35202  baerlem5abmN  35203  mapdindp0  35204  mapdheq4lem  35216  mapdheq4  35217  mapdh6lem1N  35218  mapdh6lem2N  35219  mapdh7eN  35233  mapdh7cN  35234  mapdh7fN  35236  mapdh75e  35237  mapdh75fN  35240  mapdh8aa  35261  mapdh8d0N  35267  mapdh8d  35268  hdmap1eq2  35291  hdmap1eq4N  35292  hdmap1l6lem1  35293  hdmap1l6lem2  35294  hdmap1neglem1N  35313  hdmaprnlem7N  35343  hdmaprnlem17N  35351
  Copyright terms: Public domain W3C validator