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

Theorem eqeltrrd 2358
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 2288 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2357 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  3eltr3d  2363  tz7.7  4418  xpexr2  5115  fvmptdv2  5613  ffvresb  5690  2ndrn  6168  1st2ndbr  6169  elopabi  6185  cnvf1olem  6216  dftpos4  6253  riotasvd  6347  seqomlem4  6465  oneo  6579  oeordi  6585  oeeulem  6599  oeeui  6600  nnmordi  6629  nnneo  6649  th3qlem1  6764  disjen  7018  fnfi  7134  elfi2  7168  marypha2  7192  fisupcl  7218  ordiso2  7230  ordtypelem9  7241  hartogslem2  7258  unxpwdom2  7302  noinfep  7360  cantnflt  7373  cantnfp1lem3  7382  cantnflem1  7391  cantnflem3  7393  cantnf  7395  cnfcom3lem  7406  r1pwss  7456  r0weon  7640  alephfp  7735  dfac2a  7756  cfsmolem  7896  enfin2i  7947  ac6num  8106  ttukeylem7  8142  fpwwe2lem9  8260  canthp1lem2  8275  pwfseqlem4  8284  gchaleph2  8298  wunun  8332  r1tskina  8404  tskun  8408  gruen  8434  subf  9053  resubcl  9111  negcon1ad  9152  subeq0bd  9209  rimul  9737  peano2nn  9758  nn0nnaddcl  9996  elnn0nn  10006  elz2  10040  zsubcl  10061  zrevaddcl  10063  zdiv  10082  peano5uzi  10100  peano2uzr  10274  uzaddcl  10275  qsubcl  10335  qrevaddcl  10338  icoshftf1o  10759  lincmb01cmp  10777  xov1plusxeqvd  10780  fseq1p1m1  10857  om2uzrani  11015  uzrdglem  11020  seqf1olem2  11086  expaddzlem  11145  expaddz  11146  expmulz  11148  zesq  11224  bcm1k  11327  bccl  11334  permnn  11336  hashcl  11350  hashf1lem2  11394  hashf1  11395  seqcoll  11401  shftuz  11564  ref  11597  imf  11598  crre  11599  rereb  11605  absf  11821  lo1res2  12036  o1res2  12037  o1add2  12097  o1mul2  12098  o1sub2  12099  lo1sub  12104  isercoll2  12142  summolem2a  12188  fsumf1o  12196  fsumcnv  12236  fsumshft  12242  geolim2  12327  ruclem12  12519  sqr2irrlem  12526  oexpneg  12590  3dvds  12591  bitsf1  12637  gcdf  12698  sqnprm  12777  fnum  12813  fden  12814  phimullem  12847  pc2dvds  12931  gzsubcl  12987  4sqlem5  12989  4sqlem9  12993  4sqlem10  12994  mul4sqlem  13000  mul4sq  13001  4sqlem11  13002  4sqlem13  13004  4sqlem16  13007  4sqlem17  13008  4sqlem18  13009  vdwlem5  13032  vdwlem8  13035  vdwlem9  13036  ramub1lem2  13074  firest  13337  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  prdsbascl  13382  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  mreincl  13501  ismred2  13505  mrcidb  13517  ssclem  13696  idffth  13807  ressffth  13812  coapm  13903  catciso  13939  evlfcl  13996  curfpropd  14007  diag2cl  14020  hofcllem  14032  hofcl  14033  yonffthlem  14056  yoniso  14059  lubprop  14114  glbprop  14119  p0le  14149  ple1  14150  isglbd  14221  subsubm  14434  mhmima  14440  frmdss2  14485  mulgdir  14592  imasgrp2  14610  subgmulg  14635  issubg2  14636  subsubg  14640  cycsubgcl  14643  isnsg3  14651  ssnmz  14659  eqger  14667  ghmrn  14696  ghmnsgima  14706  conjsubg  14714  conjnmz  14716  subggim  14730  gass  14755  mndodconglem  14856  odsubdvds  14882  sylow1lem1  14909  sylow1lem3  14911  sylow1lem4  14912  pgpssslw  14925  sylow2a  14930  sylow2blem3  14933  slwhash  14935  fislw  14936  sylow3lem2  14939  sylow3lem4  14941  sylow3lem5  14942  sylow3lem6  14943  lsmub1x  14957  lsmub2x  14958  lsmsubm  14964  lsmmod  14984  lsmdisj2  14991  subgdisj1  15000  efginvrel2  15036  efgsres  15047  efgsfo  15048  efgredleme  15052  iscygodd  15175  prmcyg  15180  gsumzsubmcl  15200  gsum2d2lem  15224  pwsgsum  15230  dprdcntz  15243  dprddisj  15244  dprdw  15245  dprdfid  15252  dprdfinv  15254  dprdfadd  15255  dprdfsub  15256  dprdfeq0  15257  dprdf11  15258  dprdsubg  15259  dprdub  15260  dprdlub  15261  dprdres  15263  dprdss  15264  dprdf1o  15267  dmdprdsplitlem  15272  dprddisj2  15274  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2  15281  dpjfval  15290  dpjidcl  15293  ablfacrplem  15300  ablfacrp  15301  ablfac1c  15306  ablfac1eu  15308  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfaclem1  15316  pgpfaclem3  15318  ablfaclem3  15322  0unit  15462  irredneg  15492  irrednegb  15493  isdrng2  15522  subrgcrng  15549  subrgin  15568  subsubrg  15571  srngcl  15620  islmodd  15633  lssvancl1  15702  lss0cl  15704  lssvacl  15711  lssvscl  15712  lssvnegcl  15713  lssincl  15722  lmhmima  15804  lmhmrnlss  15807  lspprabs  15848  lsslvec  15860  lspabs3  15874  lspdisj  15878  lspexch  15882  lsmcv  15894  lspsolv  15896  issubgrpd2  15941  issubrngd2  15943  rlmlvec  15958  lidl1el  15970  drngnidl  15981  2idlcpbl  15986  isassad  16063  issubassa2  16084  psrass1lem  16123  mvridlem  16164  mplsubrglem  16183  mplmonmul  16208  mplcoe3  16210  mplcoe2  16211  subrgasclcl  16240  mplmon2cl  16241  mplind  16243  zsssubrg  16430  cnsubrg  16432  gzrngunit  16437  zlpirlem1  16441  frgpcyg  16527  isphld  16558  css0  16589  pjfo  16615  unopn  16649  istps2OLD  16659  tsettps  16681  tgss2  16725  difopn  16771  incld  16780  iuncld  16782  indiscld  16828  mretopd  16829  resttop  16891  resttopon  16892  restfpw  16910  ordtbaslem  16918  ordtbas2  16921  ordtbas  16922  ordttopon  16923  ordtopn1  16924  ordtopn2  16925  ordtcld1  16927  ordtcld2  16928  ordtrest  16932  ordtrest2  16934  tgcn  16982  tgcnp  16983  cnpco  16996  cnt1  17078  cnrmnrm  17089  conndisj  17142  uncon  17155  2ndctop  17173  2ndcrest  17180  2ndcctbss  17181  2ndcomap  17184  dis2ndc  17186  restnlly  17208  islly2  17210  llyidm  17214  nllyidm  17215  dislly  17223  kgeni  17232  kgencmp2  17241  iskgen2  17243  kgencn2  17252  kgencn3  17253  elptr2  17269  ptbasfi  17276  txcld  17298  xkoccn  17313  txcn  17320  txdis  17326  txkgen  17346  xkopjcn  17350  xkococnlem  17353  cnmpt11  17357  cnmpt11f  17358  cnmpt1t  17359  cnmpt12  17361  cnmpt21  17365  cnmpt21f  17366  cnmpt2t  17367  cnmpt22  17368  cnmpt22f  17369  cnmpt1res  17370  cnmpt2res  17371  cnmptkp  17374  cnmptk1  17375  cnmpt1k  17376  cnmptkk  17377  cnmptk1p  17379  cnmptk2  17380  cnmpt2k  17382  txcon  17383  basqtop  17402  tgqtop  17403  qtopeu  17407  qtoprest  17408  qtopomap  17409  qtopcmap  17410  r0cld  17429  ordthmeolem  17492  pt1hmeo  17497  ptcmpfi  17504  xkocnv  17505  xkohmeo  17506  fbdmn0  17529  trfil1  17581  trfil2  17582  trfg  17586  uzrest  17592  uzfbas  17593  trufil  17605  elfm3  17645  rnelfm  17648  fmfnfmlem2  17650  fmfnfm  17653  txflf  17701  alexsublem  17738  alexsub  17739  alexsubb  17740  ptcmplem3  17748  ptcmplem4  17749  cnmpt1plusg  17770  cnmpt2plusg  17771  istgp2  17774  oppgtgp  17781  symgtgp  17784  subgtgp  17788  subgntr  17789  opnsubg  17790  cldsubg  17793  tgpconcomp  17795  tgpt0  17801  divstgplem  17803  divstgphaus  17805  prdstmdd  17806  tsms0  17824  tsmsadd  17829  tsmsxplem1  17835  tsmsxplem2  17836  cnmpt1vsca  17876  cnmpt2vsca  17877  xpsdsval  17945  xmeter  17979  mscl  18007  xmscl  18008  blcld  18051  stdbdxmet  18061  met2ndci  18068  ressxms  18071  ressms  18072  prdsxmslem2  18075  tmsxps  18082  tngngpd  18169  tngnrg  18185  sranlm  18195  lssnlm  18211  lssnvc  18212  xrsxmet  18315  xrsblre  18317  zdis  18322  icccmplem2  18328  xrge0tsms  18339  cnmpt1ds  18347  cnmpt2ds  18348  cncfmpt1f  18417  negcncf  18421  negfcncf  18422  cnheiborlem  18452  evth  18457  evth2  18458  lebnumlem1  18459  lebnumlem3  18461  xlebnum  18463  copco  18516  pcopt  18520  pcopt2  18521  pi1addf  18545  pi1addval  18546  pi1cof  18557  pi1coghm  18559  isclmi  18575  cphsubrglem  18613  cphreccllem  18614  cphcjcl  18619  cphsqrcl2  18622  cphsqrcl3  18623  cphqss  18624  cphnmf  18631  reipcl  18633  ipcau2  18664  cnmpt1ip  18674  cnmpt2ip  18675  clsocv  18677  iscauf  18706  cmetcaulem  18714  lmle  18727  lmcau  18738  lssbn  18773  hlprlem  18784  ishl2  18787  minveclem3b  18792  pjthlem2  18802  ovolfcl  18826  ovoliunlem1  18861  ovolshftlem1  18868  ovolicc2lem3  18878  ovolicc2lem4  18879  shftmbl  18896  inmbl  18899  difmbl  18900  volinun  18903  volfiniun  18904  voliunlem3  18909  volsup  18913  icombl1  18920  icombl  18921  ioombl  18922  iccmbl  18923  uniioombllem3  18940  uniioombllem5  18942  uniiccmbl  18945  dyaddisjlem  18950  dyadmbl  18955  opnmbllem  18956  volcn  18961  vitalilem1  18963  vitalilem4  18966  mbfdm  18983  mbfimasn  18989  mbfdm2  18993  mbfmulc2lem  19002  mbfmulc2re  19003  mbfneg  19005  mbfpos  19006  mbfposr  19007  mbfposb  19008  ismbf3d  19009  mbfimaopnlem  19010  cncombf  19013  mbfaddlem  19015  mbfadd  19016  mbfsub  19017  mbfmulc2  19018  mbflimsup  19021  mbflimlem  19022  i1fima  19033  i1fima2  19034  i1fima2sn  19035  i1fd  19036  i1f0rn  19037  itg11  19046  i1faddlem  19048  i1fadd  19050  i1fmul  19051  itg1addlem2  19052  itg1addlem4  19054  itg1addlem5  19055  itg1mulc  19059  i1fres  19060  i1fposd  19062  i1fsub  19063  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flimlem  19077  mbfi1flim  19078  mbfmullem2  19079  mbfmul  19081  itg2const  19095  itg2const2  19096  itg2seq  19097  itg2splitlem  19103  itg2monolem1  19105  itg2mono  19108  itg2gt0  19115  itg2cnlem1  19116  iblss  19159  i1fibl  19162  itgitg1  19163  itgss3  19169  ibladd  19175  iblsub  19176  iblabs  19183  bddmulibl  19193  bddibl  19194  cnmptlimc  19240  limccnp  19241  limccnp2  19242  limcco  19243  perfdvf  19253  dvcnp2  19269  cpnord  19284  cpncn  19285  cpnres  19286  dvcnvlem  19323  cmvth  19338  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip1  19344  c1lip2  19345  dvgt0lem1  19349  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem2  19365  dvcnvre  19366  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  ftc1lem1  19382  ftc1lem2  19383  ftc1a  19384  ftc1lem4  19386  ftc2  19391  ftc2ditglem  19392  ftc2ditg  19393  itgsubstlem  19395  evlsval2  19404  mpfconst  19422  mpfproj  19423  mpfaddcl  19426  mpfmulcl  19427  pf1const  19429  pf1id  19430  pf1subrg  19431  mpfpf1  19434  pf1addcl  19436  pf1mulcl  19437  pf1ind  19438  tdeglem4  19446  deg1pwle  19505  deg1submon1p  19538  plyco0  19574  elplyd  19584  plypow  19587  plyconst  19588  plypf1  19594  plysub  19601  dgrcolem1  19654  dgrcolem2  19655  vieta1lem1  19690  vieta1lem2  19691  iaa  19705  aalioulem1  19712  aalioulem4  19715  aaliou3lem6  19728  tayl0  19741  taylpfval  19744  taylthlem2  19753  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  mbfulm  19782  iblulm  19783  itgulm  19784  psercn2  19799  psercn  19802  abelthlem1  19807  abelthlem3  19809  abelth  19817  abelth2  19818  sincn  19820  coscn  19821  efcvx  19825  pige3  19885  cosne0  19892  tanregt0  19901  efif1olem4  19907  relogcl  19932  logcn  19994  dvloglem  19995  logf1o2  19997  efopnlem2  20004  logccv  20010  cxpsqr  20050  loglesqr  20098  ang180lem1  20107  ang180lem2  20108  isosctrlem2  20119  angpined  20127  mcubic  20143  atanbnd  20222  atans2  20227  atantayl2  20234  atantayl3  20235  leibpi  20238  rlimcnp2  20261  efrlim  20264  cvxcl  20279  jensen  20283  emcllem6  20294  fsumharmonic  20305  ftalem2  20311  ftalem7  20316  basellem2  20319  basellem3  20320  basellem5  20322  basellem9  20326  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  efchtdvds  20397  fsumdvdsmul  20435  chtublem  20450  fsumvma  20452  mersenne  20466  perfect  20470  dchrfi  20494  lgsne0  20572  lgseisenlem4  20591  lgsquadlem1  20593  2sqblem  20616  chebbnd2  20626  chto1lb  20627  rpvmasumlem  20636  dchrisumlem2  20639  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrmusumlem  20671  dchrvmasumlem  20672  rpvmasum  20675  rplogsum  20676  mudivsum  20679  mulog2sumlem3  20685  2vmadivsumlem  20689  selberglem2  20695  selberg2lem  20699  logdivbnd  20705  selberg3lem1  20706  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd2  20736  pntlemo  20756  ablomul  21022  ghgrp  21035  rngoablo2  21089  vcoprne  21135  nvi  21170  ipval2lem3  21278  ipval2lem6  21284  ipf  21289  ubthlem1  21449  minvecolem2  21454  minvecolem4a  21456  hhshsslem2  21845  shsel1  21900  pjoccl  22012  5oalem1  22233  5oalem5  22237  3oalem2  22242  pjrni  22281  hmopd  22602  imaelshi  22638  adjbdlnb  22664  adjsslnop  22667  bracnlnval  22694  hmopidmchi  22731  ballotlemsf1o  23072  ballotlemrinv0  23091  eldmgm  23105  erdszelem8  23140  pconcon  23173  ptpcon  23175  txsconlem  23182  rescon  23188  cvmscld  23215  cvmliftmolem1  23223  cvmliftlem1  23227  cvmliftlem8  23234  cvmlift2lem9  23253  iseupa  23292  circum  23418  setlikespec  23598  wfrlem15  23681  onsuctop  24283  areacirclem4  24339  npincppr  24571  supdef  24674  stfincomp  25003  rcmob  25161  idmorimor  25359  rocatval  25371  cmp2morpgrp  25375  cmpidmor2  25381  pgapspf  25464  pgapspf2  25465  isfne4  25681  islocfin  25708  neibastop1  25720  fnejoin2  25730  unirep  25761  sdclem2  25864  geomcau  25887  ssbnd  25924  prdsbnd2  25931  divrngcl  26000  1idl  26063  inidl  26067  prnc  26104  ispridlc  26107  elrfi  26181  mzpaddmpt  26231  mzpmulmpt  26232  diophun  26265  elpell1qr2  26369  pellfundglb  26382  qirropth  26405  rmspecfund  26406  rmbaserp  26416  rmxnn  26450  jm2.27a  26510  jm2.27c  26512  fnwe2lem3  26561  lnmfg  26592  kercvrlsm  26593  lnmepi  26595  pwssplit4  26603  frlmgsum  26644  uvcresum  26654  frlmsplit2  26655  frlmup1  26662  hbtlem5  26744  hbt  26746  rngunsnply  26790  symggen  26823  psgnunilem1  26828  psgnunilem3  26831  acsfn1p  26919  rfcnpre1  27102  refsumcn  27113  rfcnpre2  27114  refsum2cnlem1  27120  mulc1cncfg  27133  stoweidlem9  27170  stoweidlem17  27178  stoweidlem19  27180  stoweidlem20  27181  stoweidlem23  27184  stoweidlem31  27192  stoweidlem41  27202  stoweidlem47  27208  stirlinglem3  27237  stirlinglem7  27241  stirlinglem8  27242  stirlinglem11  27245  stirlinglem15  27249  sigardiv  27263  afvelrn  27442  bnj1145  28396  lkrlsp  28665  glbconN  28939  cvratlem  28983  llncvrlpln  29120  lplncvrlvol  29178  psubclsubN  29502  psubclinN  29510  4atexlemcnd  29634  cdleme23b  29912  cdlemk35  30474  dvaabl  30587  dia1elN  30617  diaintclN  30621  diasslssN  30622  dia2dimlem7  30633  dvadiaN  30691  dibintclN  30730  dihopelvalcpre  30811  dihsslss  30839  dih0rn  30847  dih1rn  30850  dihintcl  30907  dihmeetcl  30908  dochocss  30929  dochoccl  30932  dochsat  30946  dihsmsprn  30993  dochsnshp  31016  dochexmidlem6  31028  lcfl8b  31067  lclkrlem2g  31076  mapdpglem5N  31240  mapdpglem9  31243  mapdpglem14  31248  mapdpglem30a  31258  mapdpglem30b  31259  baerlem5amN  31279  baerlem5bmN  31280  baerlem5abmN  31281  mapdindp0  31282  mapdheq4lem  31294  mapdheq4  31295  mapdh6lem1N  31296  mapdh6lem2N  31297  mapdh7eN  31311  mapdh7cN  31312  mapdh7fN  31314  mapdh75e  31315  mapdh75fN  31318  mapdh8aa  31339  mapdh8d0N  31345  mapdh8d  31346  hdmap1eq2  31369  hdmap1eq4N  31370  hdmap1l6lem1  31371  hdmap1l6lem2  31372  hdmap1neglem1N  31391  hdmaprnlem7N  31421  hdmaprnlem17N  31429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator