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

Theorem eqeltrrd 2371
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 2301 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2370 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  3eltr3d  2376  tz7.7  4434  xpexr2  5131  fvmptdv2  5629  ffvresb  5706  2ndrn  6184  1st2ndbr  6185  elopabi  6201  cnvf1olem  6232  dftpos4  6269  riotasvd  6363  seqomlem4  6481  oneo  6595  oeordi  6601  oeeulem  6615  oeeui  6616  nnmordi  6645  nnneo  6665  th3qlem1  6780  disjen  7034  fnfi  7150  elfi2  7184  marypha2  7208  fisupcl  7234  ordiso2  7246  ordtypelem9  7257  hartogslem2  7274  unxpwdom2  7318  noinfep  7376  cantnflt  7389  cantnfp1lem3  7398  cantnflem1  7407  cantnflem3  7409  cantnf  7411  cnfcom3lem  7422  r1pwss  7472  r0weon  7656  alephfp  7751  dfac2a  7772  cfsmolem  7912  enfin2i  7963  ac6num  8122  ttukeylem7  8158  fpwwe2lem9  8276  canthp1lem2  8291  pwfseqlem4  8300  gchaleph2  8314  wunun  8348  r1tskina  8420  tskun  8424  gruen  8450  subf  9069  resubcl  9127  negcon1ad  9168  subeq0bd  9225  rimul  9753  peano2nn  9774  nn0nnaddcl  10012  elnn0nn  10022  elz2  10056  zsubcl  10077  zrevaddcl  10079  zdiv  10098  peano5uzi  10116  peano2uzr  10290  uzaddcl  10291  qsubcl  10351  qrevaddcl  10354  icoshftf1o  10775  lincmb01cmp  10793  xov1plusxeqvd  10796  fseq1p1m1  10873  om2uzrani  11031  uzrdglem  11036  seqf1olem2  11102  expaddzlem  11161  expaddz  11162  expmulz  11164  zesq  11240  bcm1k  11343  bccl  11350  permnn  11352  hashcl  11366  hashf1lem2  11410  hashf1  11411  seqcoll  11417  shftuz  11580  ref  11613  imf  11614  crre  11615  rereb  11621  absf  11837  lo1res2  12052  o1res2  12053  o1add2  12113  o1mul2  12114  o1sub2  12115  lo1sub  12120  isercoll2  12158  summolem2a  12204  fsumf1o  12212  fsumcnv  12252  fsumshft  12258  geolim2  12343  ruclem12  12535  sqr2irrlem  12542  oexpneg  12606  3dvds  12607  bitsf1  12653  gcdf  12714  sqnprm  12793  fnum  12829  fden  12830  phimullem  12863  pc2dvds  12947  gzsubcl  13003  4sqlem5  13005  4sqlem9  13009  4sqlem10  13010  mul4sqlem  13016  mul4sq  13017  4sqlem11  13018  4sqlem13  13020  4sqlem16  13023  4sqlem17  13024  4sqlem18  13025  vdwlem5  13048  vdwlem8  13051  vdwlem9  13052  ramub1lem2  13090  firest  13353  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  prdsbascl  13398  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  mreincl  13517  ismred2  13521  mrcidb  13533  ssclem  13712  idffth  13823  ressffth  13828  coapm  13919  catciso  13955  evlfcl  14012  curfpropd  14023  diag2cl  14036  hofcllem  14048  hofcl  14049  yonffthlem  14072  yoniso  14075  lubprop  14130  glbprop  14135  p0le  14165  ple1  14166  isglbd  14237  subsubm  14450  mhmima  14456  frmdss2  14501  mulgdir  14608  imasgrp2  14626  subgmulg  14651  issubg2  14652  subsubg  14656  cycsubgcl  14659  isnsg3  14667  ssnmz  14675  eqger  14683  ghmrn  14712  ghmnsgima  14722  conjsubg  14730  conjnmz  14732  subggim  14746  gass  14771  mndodconglem  14872  odsubdvds  14898  sylow1lem1  14925  sylow1lem3  14927  sylow1lem4  14928  pgpssslw  14941  sylow2a  14946  sylow2blem3  14949  slwhash  14951  fislw  14952  sylow3lem2  14955  sylow3lem4  14957  sylow3lem5  14958  sylow3lem6  14959  lsmub1x  14973  lsmub2x  14974  lsmsubm  14980  lsmmod  15000  lsmdisj2  15007  subgdisj1  15016  efginvrel2  15052  efgsres  15063  efgsfo  15064  efgredleme  15068  iscygodd  15191  prmcyg  15196  gsumzsubmcl  15216  gsum2d2lem  15240  pwsgsum  15246  dprdcntz  15259  dprddisj  15260  dprdw  15261  dprdfid  15268  dprdfinv  15270  dprdfadd  15271  dprdfsub  15272  dprdfeq0  15273  dprdf11  15274  dprdsubg  15275  dprdub  15276  dprdlub  15277  dprdres  15279  dprdss  15280  dprdf1o  15283  dmdprdsplitlem  15288  dprddisj2  15290  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2  15297  dpjfval  15306  dpjidcl  15309  ablfacrplem  15316  ablfacrp  15317  ablfac1c  15322  ablfac1eu  15324  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfaclem1  15332  pgpfaclem3  15334  ablfaclem3  15338  0unit  15478  irredneg  15508  irrednegb  15509  isdrng2  15538  subrgcrng  15565  subrgin  15584  subsubrg  15587  srngcl  15636  islmodd  15649  lssvancl1  15718  lss0cl  15720  lssvacl  15727  lssvscl  15728  lssvnegcl  15729  lssincl  15738  lmhmima  15820  lmhmrnlss  15823  lspprabs  15864  lsslvec  15876  lspabs3  15890  lspdisj  15894  lspexch  15898  lsmcv  15910  lspsolv  15912  issubgrpd2  15957  issubrngd2  15959  rlmlvec  15974  lidl1el  15986  drngnidl  15997  2idlcpbl  16002  isassad  16079  issubassa2  16100  psrass1lem  16139  mvridlem  16180  mplsubrglem  16199  mplmonmul  16224  mplcoe3  16226  mplcoe2  16227  subrgasclcl  16256  mplmon2cl  16257  mplind  16259  zsssubrg  16446  cnsubrg  16448  gzrngunit  16453  zlpirlem1  16457  frgpcyg  16543  isphld  16574  css0  16605  pjfo  16631  unopn  16665  istps2OLD  16675  tsettps  16697  tgss2  16741  difopn  16787  incld  16796  iuncld  16798  indiscld  16844  mretopd  16845  resttop  16907  resttopon  16908  restfpw  16926  ordtbaslem  16934  ordtbas2  16937  ordtbas  16938  ordttopon  16939  ordtopn1  16940  ordtopn2  16941  ordtcld1  16943  ordtcld2  16944  ordtrest  16948  ordtrest2  16950  tgcn  16998  tgcnp  16999  cnpco  17012  cnt1  17094  cnrmnrm  17105  conndisj  17158  uncon  17171  2ndctop  17189  2ndcrest  17196  2ndcctbss  17197  2ndcomap  17200  dis2ndc  17202  restnlly  17224  islly2  17226  llyidm  17230  nllyidm  17231  dislly  17239  kgeni  17248  kgencmp2  17257  iskgen2  17259  kgencn2  17268  kgencn3  17269  elptr2  17285  ptbasfi  17292  txcld  17314  xkoccn  17329  txcn  17336  txdis  17342  txkgen  17362  xkopjcn  17366  xkococnlem  17369  cnmpt11  17373  cnmpt11f  17374  cnmpt1t  17375  cnmpt12  17377  cnmpt21  17381  cnmpt21f  17382  cnmpt2t  17383  cnmpt22  17384  cnmpt22f  17385  cnmpt1res  17386  cnmpt2res  17387  cnmptkp  17390  cnmptk1  17391  cnmpt1k  17392  cnmptkk  17393  cnmptk1p  17395  cnmptk2  17396  cnmpt2k  17398  txcon  17399  basqtop  17418  tgqtop  17419  qtopeu  17423  qtoprest  17424  qtopomap  17425  qtopcmap  17426  r0cld  17445  ordthmeolem  17508  pt1hmeo  17513  ptcmpfi  17520  xkocnv  17521  xkohmeo  17522  fbdmn0  17545  trfil1  17597  trfil2  17598  trfg  17602  uzrest  17608  uzfbas  17609  trufil  17621  elfm3  17661  rnelfm  17664  fmfnfmlem2  17666  fmfnfm  17669  txflf  17717  alexsublem  17754  alexsub  17755  alexsubb  17756  ptcmplem3  17764  ptcmplem4  17765  cnmpt1plusg  17786  cnmpt2plusg  17787  istgp2  17790  oppgtgp  17797  symgtgp  17800  subgtgp  17804  subgntr  17805  opnsubg  17806  cldsubg  17809  tgpconcomp  17811  tgpt0  17817  divstgplem  17819  divstgphaus  17821  prdstmdd  17822  tsms0  17840  tsmsadd  17845  tsmsxplem1  17851  tsmsxplem2  17852  cnmpt1vsca  17892  cnmpt2vsca  17893  xpsdsval  17961  xmeter  17995  mscl  18023  xmscl  18024  blcld  18067  stdbdxmet  18077  met2ndci  18084  ressxms  18087  ressms  18088  prdsxmslem2  18091  tmsxps  18098  tngngpd  18185  tngnrg  18201  sranlm  18211  lssnlm  18227  lssnvc  18228  xrsxmet  18331  xrsblre  18333  zdis  18338  icccmplem2  18344  xrge0tsms  18355  cnmpt1ds  18363  cnmpt2ds  18364  cncfmpt1f  18433  negcncf  18437  negfcncf  18438  cnheiborlem  18468  evth  18473  evth2  18474  lebnumlem1  18475  lebnumlem3  18477  xlebnum  18479  copco  18532  pcopt  18536  pcopt2  18537  pi1addf  18561  pi1addval  18562  pi1cof  18573  pi1coghm  18575  isclmi  18591  cphsubrglem  18629  cphreccllem  18630  cphcjcl  18635  cphsqrcl2  18638  cphsqrcl3  18639  cphqss  18640  cphnmf  18647  reipcl  18649  ipcau2  18680  cnmpt1ip  18690  cnmpt2ip  18691  clsocv  18693  iscauf  18722  cmetcaulem  18730  lmle  18743  lmcau  18754  lssbn  18789  hlprlem  18800  ishl2  18803  minveclem3b  18808  pjthlem2  18818  ovolfcl  18842  ovoliunlem1  18877  ovolshftlem1  18884  ovolicc2lem3  18894  ovolicc2lem4  18895  shftmbl  18912  inmbl  18915  difmbl  18916  volinun  18919  volfiniun  18920  voliunlem3  18925  volsup  18929  icombl1  18936  icombl  18937  ioombl  18938  iccmbl  18939  uniioombllem3  18956  uniioombllem5  18958  uniiccmbl  18961  dyaddisjlem  18966  dyadmbl  18971  opnmbllem  18972  volcn  18977  vitalilem1  18979  vitalilem4  18982  mbfdm  18999  mbfimasn  19005  mbfdm2  19009  mbfmulc2lem  19018  mbfmulc2re  19019  mbfneg  19021  mbfpos  19022  mbfposr  19023  mbfposb  19024  ismbf3d  19025  mbfimaopnlem  19026  cncombf  19029  mbfaddlem  19031  mbfadd  19032  mbfsub  19033  mbfmulc2  19034  mbflimsup  19037  mbflimlem  19038  i1fima  19049  i1fima2  19050  i1fima2sn  19051  i1fd  19052  i1f0rn  19053  itg11  19062  i1faddlem  19064  i1fadd  19066  i1fmul  19067  itg1addlem2  19068  itg1addlem4  19070  itg1addlem5  19071  itg1mulc  19075  i1fres  19076  i1fposd  19078  i1fsub  19079  itg1climres  19085  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1flimlem  19093  mbfi1flim  19094  mbfmullem2  19095  mbfmul  19097  itg2const  19111  itg2const2  19112  itg2seq  19113  itg2splitlem  19119  itg2monolem1  19121  itg2mono  19124  itg2gt0  19131  itg2cnlem1  19132  iblss  19175  i1fibl  19178  itgitg1  19179  itgss3  19185  ibladd  19191  iblsub  19192  iblabs  19199  bddmulibl  19209  bddibl  19210  cnmptlimc  19256  limccnp  19257  limccnp2  19258  limcco  19259  perfdvf  19269  dvcnp2  19285  cpnord  19300  cpncn  19301  cpnres  19302  dvcnvlem  19339  cmvth  19354  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  c1lip1  19360  c1lip2  19361  dvgt0lem1  19365  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvrelem2  19381  dvcnvre  19382  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  ftc1lem1  19398  ftc1lem2  19399  ftc1a  19400  ftc1lem4  19402  ftc2  19407  ftc2ditglem  19408  ftc2ditg  19409  itgsubstlem  19411  evlsval2  19420  mpfconst  19438  mpfproj  19439  mpfaddcl  19442  mpfmulcl  19443  pf1const  19445  pf1id  19446  pf1subrg  19447  mpfpf1  19450  pf1addcl  19452  pf1mulcl  19453  pf1ind  19454  tdeglem4  19462  deg1pwle  19521  deg1submon1p  19554  plyco0  19590  elplyd  19600  plypow  19603  plyconst  19604  plypf1  19610  plysub  19617  dgrcolem1  19670  dgrcolem2  19671  vieta1lem1  19706  vieta1lem2  19707  iaa  19721  aalioulem1  19728  aalioulem4  19731  aaliou3lem6  19744  tayl0  19757  taylpfval  19760  taylthlem2  19769  ulmdvlem1  19793  ulmdvlem3  19795  mtest  19797  mbfulm  19798  iblulm  19799  itgulm  19800  psercn2  19815  psercn  19818  abelthlem1  19823  abelthlem3  19825  abelth  19833  abelth2  19834  sincn  19836  coscn  19837  efcvx  19841  pige3  19901  cosne0  19908  tanregt0  19917  efif1olem4  19923  relogcl  19948  logcn  20010  dvloglem  20011  logf1o2  20013  efopnlem2  20020  logccv  20026  cxpsqr  20066  loglesqr  20114  ang180lem1  20123  ang180lem2  20124  isosctrlem2  20135  angpined  20143  mcubic  20159  atanbnd  20238  atans2  20243  atantayl2  20250  atantayl3  20251  leibpi  20254  rlimcnp2  20277  efrlim  20280  cvxcl  20295  jensen  20299  emcllem6  20310  fsumharmonic  20321  ftalem2  20327  ftalem7  20332  basellem2  20335  basellem3  20336  basellem5  20338  basellem9  20342  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  efchtdvds  20413  fsumdvdsmul  20451  chtublem  20466  fsumvma  20468  mersenne  20482  perfect  20486  dchrfi  20510  lgsne0  20588  lgseisenlem4  20607  lgsquadlem1  20609  2sqblem  20632  chebbnd2  20642  chto1lb  20643  rpvmasumlem  20652  dchrisumlem2  20655  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrmusumlem  20687  dchrvmasumlem  20688  rpvmasum  20691  rplogsum  20692  mudivsum  20695  mulog2sumlem3  20701  2vmadivsumlem  20705  selberglem2  20711  selberg2lem  20715  logdivbnd  20721  selberg3lem1  20722  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd2  20752  pntlemo  20772  ablomul  21038  ghgrp  21051  rngoablo2  21105  vcoprne  21151  nvi  21186  ipval2lem3  21294  ipval2lem6  21300  ipf  21305  ubthlem1  21465  minvecolem2  21470  minvecolem4a  21472  hhshsslem2  21861  shsel1  21916  pjoccl  22028  5oalem1  22249  5oalem5  22253  3oalem2  22258  pjrni  22297  hmopd  22618  imaelshi  22654  adjbdlnb  22680  adjsslnop  22683  bracnlnval  22710  hmopidmchi  22747  ballotlemsf1o  23088  ballotlemrinv0  23107  disjabrex  23374  disjabrexf  23375  lmxrge0  23390  xrge0tsmsd  23397  esumf1o  23444  esumpcvgval  23461  esumcvg  23469  unelsiga  23510  cldssbrsiga  23533  indf1ofs  23624  eldmgm  23709  erdszelem8  23744  pconcon  23777  ptpcon  23779  txsconlem  23786  rescon  23792  cvmscld  23819  cvmliftmolem1  23827  cvmliftlem1  23831  cvmliftlem8  23838  cvmlift2lem9  23857  iseupa  23896  circum  24022  prodmolem2a  24157  fprodf1o  24172  setlikespec  24258  wfrlem15  24341  onsuctop  24944  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itgaddnclem2  25010  itgaddnc  25011  iblsubnc  25012  itgmulc2nclem2  25018  itgmulc2nc  25019  itgabsnc  25020  bddiblnc  25021  ftc1cnnclem  25024  areacirclem4  25030  npincppr  25262  supdef  25365  stfincomp  25694  rcmob  25852  idmorimor  26050  rocatval  26062  cmp2morpgrp  26066  cmpidmor2  26072  pgapspf  26155  pgapspf2  26156  isfne4  26372  islocfin  26399  neibastop1  26411  fnejoin2  26421  unirep  26452  sdclem2  26555  geomcau  26578  ssbnd  26615  prdsbnd2  26622  divrngcl  26691  1idl  26754  inidl  26758  prnc  26795  ispridlc  26798  elrfi  26872  mzpaddmpt  26922  mzpmulmpt  26923  diophun  26956  elpell1qr2  27060  pellfundglb  27073  qirropth  27096  rmspecfund  27097  rmbaserp  27107  rmxnn  27141  jm2.27a  27201  jm2.27c  27203  fnwe2lem3  27252  lnmfg  27283  kercvrlsm  27284  lnmepi  27286  pwssplit4  27294  frlmgsum  27335  uvcresum  27345  frlmsplit2  27346  frlmup1  27353  hbtlem5  27435  hbt  27437  rngunsnply  27481  symggen  27514  psgnunilem1  27519  psgnunilem3  27522  acsfn1p  27610  rfcnpre1  27793  refsumcn  27804  rfcnpre2  27805  refsum2cnlem1  27811  mulc1cncfg  27824  stoweidlem9  27861  stoweidlem17  27869  stoweidlem19  27871  stoweidlem20  27872  stoweidlem23  27875  stoweidlem31  27883  stoweidlem41  27893  stoweidlem47  27899  stirlinglem3  27928  stirlinglem7  27932  stirlinglem8  27933  stirlinglem11  27936  stirlinglem15  27940  sigardiv  27954  afvelrn  28136  bnj1145  29339  lkrlsp  29914  glbconN  30188  cvratlem  30232  llncvrlpln  30369  lplncvrlvol  30427  psubclsubN  30751  psubclinN  30759  4atexlemcnd  30883  cdleme23b  31161  cdlemk35  31723  dvaabl  31836  dia1elN  31866  diaintclN  31870  diasslssN  31871  dia2dimlem7  31882  dvadiaN  31940  dibintclN  31979  dihopelvalcpre  32060  dihsslss  32088  dih0rn  32096  dih1rn  32099  dihintcl  32156  dihmeetcl  32157  dochocss  32178  dochoccl  32181  dochsat  32195  dihsmsprn  32242  dochsnshp  32265  dochexmidlem6  32277  lcfl8b  32316  lclkrlem2g  32325  mapdpglem5N  32489  mapdpglem9  32492  mapdpglem14  32497  mapdpglem30a  32507  mapdpglem30b  32508  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdindp0  32531  mapdheq4lem  32543  mapdheq4  32544  mapdh6lem1N  32545  mapdh6lem2N  32546  mapdh7eN  32560  mapdh7cN  32561  mapdh7fN  32563  mapdh75e  32564  mapdh75fN  32567  mapdh8aa  32588  mapdh8d0N  32594  mapdh8d  32595  hdmap1eq2  32618  hdmap1eq4N  32619  hdmap1l6lem1  32620  hdmap1l6lem2  32621  hdmap1neglem1N  32640  hdmaprnlem7N  32670  hdmaprnlem17N  32678
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator