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

Theorem eqeltrrd 2510
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 2440 . 2  |-  ( ph  ->  B  =  A )
3 eqeltrrd.2 . 2  |-  ( ph  ->  A  e.  C )
42, 3eqeltrd 2509 1  |-  ( ph  ->  B  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  3eltr3d  2515  tz7.7  4599  xpexr2  5300  fvmptdv2  5810  ffvresb  5892  2ndrn  6387  1st2ndbr  6388  elopabi  6404  cnvf1olem  6436  dftpos4  6490  riotasvd  6584  seqomlem4  6702  oneo  6816  oeordi  6822  oeeulem  6836  oeeui  6837  nnmordi  6866  nnneo  6886  th3qlem1  7002  disjen  7256  fnfi  7376  elfi2  7411  fisupcl  7464  ordiso2  7476  ordtypelem9  7487  hartogslem2  7504  unxpwdom2  7548  noinfep  7606  cantnflt  7619  cantnfp1lem3  7628  cantnflem1  7637  cantnflem3  7639  cantnf  7641  cnfcom3lem  7652  r1pwss  7702  r0weon  7886  alephfp  7981  dfac2a  8002  cfsmolem  8142  enfin2i  8193  ac6num  8351  ttukeylem7  8387  fpwwe2lem9  8505  canthp1lem2  8520  pwfseqlem4  8529  gchaleph2  8543  wunun  8577  r1tskina  8649  tskun  8653  gruen  8679  subf  9299  resubcl  9357  negcon1ad  9398  subeq0bd  9455  rimul  9983  peano2nn  10004  nn0nnaddcl  10244  elnn0nn  10254  elz2  10290  zsubcl  10311  zrevaddcl  10313  zdiv  10332  peano5uzi  10350  peano2uzr  10524  uzaddcl  10525  qsubcl  10585  qrevaddcl  10588  xov1plusxeqvd  11033  fseq1p1m1  11114  om2uzrani  11284  uzrdglem  11289  seqf1olem2  11355  expaddzlem  11415  expaddz  11416  expmulz  11418  zesq  11494  bcm1k  11598  bccl  11605  permnn  11609  hashcl  11631  hashf1lem2  11697  hashf1  11698  seqcoll  11704  shftuz  11876  ref  11909  imf  11910  crre  11911  rereb  11917  absf  12133  lo1res2  12348  o1res2  12349  o1add2  12409  o1mul2  12410  o1sub2  12411  lo1sub  12416  isercoll2  12454  summolem2a  12501  fsumf1o  12509  fsumcnv  12549  fsumshft  12555  geolim2  12640  ruclem12  12832  sqr2irrlem  12839  oexpneg  12903  3dvds  12904  bitsf1  12950  gcdf  13011  sqnprm  13090  fnum  13126  fden  13127  phimullem  13160  pc2dvds  13244  gzsubcl  13300  4sqlem5  13302  4sqlem9  13306  4sqlem10  13307  mul4sqlem  13313  mul4sq  13314  4sqlem11  13315  4sqlem13  13317  4sqlem16  13320  4sqlem17  13321  4sqlem18  13322  vdwlem5  13345  vdwlem8  13348  vdwlem9  13349  ramub1lem2  13387  firest  13652  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  prdshom  13681  prdsbascl  13697  xpsaddlem  13792  xpsvsca  13796  xpsle  13798  mreincl  13816  ismred2  13820  mrcidb  13832  ssclem  14011  idffth  14122  ressffth  14127  coapm  14218  catciso  14254  evlfcl  14311  diag2cl  14335  hofcllem  14347  hofcl  14348  yonffthlem  14371  yoniso  14374  lubprop  14429  glbprop  14434  p0le  14464  ple1  14465  isglbd  14536  subsubm  14749  mhmima  14755  frmdss2  14800  mulgdir  14907  imasgrp2  14925  subgmulg  14950  issubg2  14951  subsubg  14955  cycsubgcl  14958  isnsg3  14966  ssnmz  14974  eqger  14982  ghmrn  15011  ghmnsgima  15021  conjsubg  15029  conjnmz  15031  subggim  15045  gass  15070  mndodconglem  15171  odsubdvds  15197  sylow1lem1  15224  sylow1lem3  15226  sylow1lem4  15227  pgpssslw  15240  sylow2a  15245  sylow2blem3  15248  slwhash  15250  fislw  15251  sylow3lem2  15254  sylow3lem4  15256  sylow3lem5  15257  sylow3lem6  15258  lsmub1x  15272  lsmub2x  15273  lsmsubm  15279  lsmmod  15299  lsmdisj2  15306  subgdisj1  15315  efginvrel2  15351  efgsres  15362  efgsfo  15363  efgredleme  15367  iscygodd  15490  prmcyg  15495  gsumzsubmcl  15515  gsum2d2lem  15539  pwsgsum  15545  dprdcntz  15558  dprddisj  15559  dprdw  15560  dprdfid  15567  dprdfinv  15569  dprdfadd  15570  dprdfsub  15571  dprdfeq0  15572  dprdf11  15573  dprdsubg  15574  dprdub  15575  dprdlub  15576  dprdres  15578  dprdss  15579  dprdf1o  15582  dmdprdsplitlem  15587  dprddisj2  15589  dprd2dlem2  15590  dprd2dlem1  15591  dprd2da  15592  dmdprdsplit2  15596  dpjfval  15605  dpjidcl  15608  ablfacrplem  15615  ablfacrp  15616  ablfac1c  15621  ablfac1eu  15623  pgpfac1lem3a  15626  pgpfac1lem3  15627  pgpfaclem1  15631  pgpfaclem3  15633  ablfaclem3  15637  0unit  15777  irredneg  15807  irrednegb  15808  isdrng2  15837  subrgcrng  15864  subrgin  15883  subsubrg  15886  srngcl  15935  islmodd  15948  lssvancl1  16013  lss0cl  16015  lssvacl  16022  lssvscl  16023  lssvnegcl  16024  lssincl  16033  lmhmima  16115  lmhmrnlss  16118  lsslvec  16171  lspabs3  16185  lspdisj  16189  lspexch  16193  lsmcv  16205  lspsolv  16207  issubgrpd2  16252  issubrngd2  16254  rlmlvec  16269  lidl1el  16281  drngnidl  16292  2idlcpbl  16297  isassad  16374  issubassa2  16395  psrass1lem  16434  mvridlem  16475  mplsubrglem  16494  mplmonmul  16519  mplcoe3  16521  mplcoe2  16522  subrgasclcl  16551  mplmon2cl  16552  mplind  16554  zsssubrg  16749  cnsubrg  16751  gzrngunit  16756  zlpirlem1  16760  frgpcyg  16846  isphld  16877  css0  16908  pjfo  16934  unopn  16968  istps2OLD  16978  tsettps  17000  tgss2  17044  difopn  17090  incld  17099  iuncld  17101  indiscld  17147  mretopd  17148  resttop  17216  resttopon  17217  restfpw  17235  ordtbaslem  17244  ordtbas2  17247  ordtbas  17248  ordttopon  17249  ordtopn1  17250  ordtopn2  17251  ordtcld1  17253  ordtcld2  17254  ordtrest  17258  ordtrest2  17260  tgcn  17308  tgcnp  17309  cnpco  17323  cnt1  17406  cnrmnrm  17417  conndisj  17471  uncon  17484  2ndctop  17502  2ndcrest  17509  2ndcctbss  17510  2ndcomap  17513  dis2ndc  17515  restnlly  17537  islly2  17539  llyidm  17543  nllyidm  17544  dislly  17552  kgeni  17561  kgencmp2  17570  iskgen2  17572  kgencn2  17581  kgencn3  17582  elptr2  17598  ptbasfi  17605  txcld  17627  xkoccn  17643  txcn  17650  txdis  17656  txkgen  17676  xkopjcn  17680  xkococnlem  17683  cnmpt11  17687  cnmpt11f  17688  cnmpt1t  17689  cnmpt12  17691  cnmpt21  17695  cnmpt21f  17696  cnmpt2t  17697  cnmpt22  17698  cnmpt22f  17699  cnmpt1res  17700  cnmptkp  17704  cnmptk1  17705  cnmpt1k  17706  cnmptkk  17707  cnmptk1p  17709  cnmptk2  17710  cnmpt2k  17712  txcon  17713  basqtop  17735  tgqtop  17736  qtopeu  17740  qtoprest  17741  qtopomap  17742  qtopcmap  17743  r0cld  17762  ordthmeolem  17825  pt1hmeo  17830  ptcmpfi  17837  xkocnv  17838  xkohmeo  17839  fbdmn0  17858  trfil1  17910  trfil2  17911  trfg  17915  uzrest  17921  uzfbas  17922  trufil  17934  elfm3  17974  rnelfm  17977  fmfnfmlem2  17979  fmfnfm  17982  txflf  18030  alexsublem  18067  alexsub  18068  alexsubb  18069  ptcmplem3  18077  ptcmplem4  18078  cnmpt1plusg  18109  cnmpt2plusg  18110  istgp2  18113  oppgtgp  18120  symgtgp  18123  subgtgp  18127  subgntr  18128  opnsubg  18129  cldsubg  18132  tgpconcomp  18134  tgpt0  18140  divstgplem  18142  divstgphaus  18144  prdstmdd  18145  tsms0  18163  tsmsadd  18168  tsmsxplem1  18174  tsmsxplem2  18175  cnmpt1vsca  18215  cnmpt2vsca  18216  trust  18251  uspreg  18296  xpsdsval  18403  xmeter  18455  mscl  18483  xmscl  18484  blcld  18527  stdbdxmet  18537  met2ndci  18544  prdsxmslem2  18551  tmsxps  18558  metustidOLD  18581  metustid  18582  tngngpd  18686  tngnrg  18702  sranlm  18712  lssnlm  18728  lssnvc  18729  xrsxmet  18832  xrsblre  18834  zdis  18839  icccmplem2  18846  xrge0tsms  18857  cnmpt1ds  18865  cnmpt2ds  18866  cncfmpt1f  18935  negcncf  18940  negfcncf  18941  cnheiborlem  18971  evth  18976  evth2  18977  lebnumlem1  18978  lebnumlem3  18980  xlebnum  18982  copco  19035  pcopt  19039  pcopt2  19040  pi1addf  19064  pi1addval  19065  pi1cof  19076  pi1coghm  19078  isclmi  19094  cphsubrglem  19132  cphreccllem  19133  cphcjcl  19138  cphsqrcl2  19141  cphsqrcl3  19142  cphqss  19143  cphnmf  19150  reipcl  19152  ipcau2  19183  cnmpt1ip  19193  cnmpt2ip  19194  clsocv  19196  iscauf  19225  cmetcaulem  19233  lmle  19246  lmcau  19257  lssbn  19296  hlprlem  19313  ishl2  19316  minveclem3b  19321  pjthlem2  19331  ovolfcl  19355  ovoliunlem1  19390  ovolshftlem1  19397  ovolicc2lem3  19407  ovolicc2lem4  19408  shftmbl  19425  inmbl  19428  difmbl  19429  volinun  19432  volfiniun  19433  voliunlem3  19438  volsup  19442  icombl1  19449  icombl  19450  ioombl  19451  iccmbl  19452  uniioombllem3  19469  uniioombllem5  19471  uniiccmbl  19474  dyaddisjlem  19479  dyadmbl  19484  opnmbllem  19485  volcn  19490  vitalilem1  19492  vitalilem4  19495  mbfdm  19512  mbfimasn  19518  mbfdm2  19522  mbfmulc2lem  19531  mbfmulc2re  19532  mbfneg  19534  mbfpos  19535  mbfposr  19536  mbfposb  19537  ismbf3d  19538  mbfimaopnlem  19539  cncombf  19542  mbfaddlem  19544  mbfadd  19545  mbfsub  19546  mbfmulc2  19547  mbflimsup  19550  mbflimlem  19551  i1fima  19562  i1fima2  19563  i1fima2sn  19564  i1fd  19565  i1f0rn  19566  itg11  19575  i1faddlem  19577  i1fadd  19579  i1fmul  19580  itg1addlem2  19581  itg1addlem4  19583  itg1addlem5  19584  itg1mulc  19588  i1fres  19589  i1fposd  19591  i1fsub  19592  itg1climres  19598  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  mbfi1flimlem  19606  mbfi1flim  19607  mbfmullem2  19608  mbfmul  19610  itg2const  19624  itg2const2  19625  itg2seq  19626  itg2splitlem  19632  itg2monolem1  19634  itg2mono  19637  itg2gt0  19644  itg2cnlem1  19645  iblss  19688  i1fibl  19691  itgitg1  19692  itgss3  19698  ibladd  19704  iblsub  19705  iblabs  19712  bddmulibl  19722  bddibl  19723  cnmptlimc  19769  limccnp  19770  limccnp2  19771  perfdvf  19782  dvcnp2  19798  cpnord  19813  cpncn  19814  cpnres  19815  dvcnvlem  19852  cmvth  19867  dvlip  19869  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  c1lip1  19873  c1lip2  19874  dvgt0lem1  19878  lhop1lem  19889  lhop2  19891  lhop  19892  dvcnvrelem2  19894  dvcnvre  19895  dvfsumle  19897  dvfsumabs  19899  dvfsumlem2  19903  ftc1lem1  19911  ftc1lem2  19912  ftc1a  19913  ftc1lem4  19915  ftc2  19920  ftc2ditglem  19921  ftc2ditg  19922  itgsubstlem  19924  evlsval2  19933  mpfconst  19951  mpfproj  19952  mpfaddcl  19955  mpfmulcl  19956  pf1const  19958  pf1id  19959  pf1subrg  19960  mpfpf1  19963  pf1addcl  19965  pf1mulcl  19966  pf1ind  19967  tdeglem4  19975  deg1pwle  20034  deg1submon1p  20067  plyco0  20103  elplyd  20113  plypow  20116  plyconst  20117  plypf1  20123  plysub  20130  dgrcolem1  20183  dgrcolem2  20184  vieta1lem1  20219  vieta1lem2  20220  iaa  20234  aalioulem1  20241  aalioulem4  20244  aaliou3lem6  20257  tayl0  20270  taylpfval  20273  taylthlem2  20282  ulmdvlem1  20308  ulmdvlem3  20310  mtest  20312  mtestbdd  20313  mbfulm  20314  iblulm  20315  itgulm  20316  psercn2  20331  psercn  20334  abelthlem1  20339  abelthlem3  20341  abelth  20349  abelth2  20350  sincn  20352  coscn  20353  efcvx  20357  pige3  20417  cosne0  20424  tanregt0  20433  efif1olem4  20439  relogcl  20465  logdiv2  20504  logcn  20530  dvloglem  20531  logf1o2  20533  efopnlem2  20540  logccv  20546  cxpsqr  20586  loglesqr  20634  ang180lem1  20643  ang180lem2  20644  isosctrlem2  20655  angpined  20663  mcubic  20679  atanbnd  20758  atans2  20763  atantayl2  20770  atantayl3  20771  leibpi  20774  rlimcnp2  20797  efrlim  20800  cvxcl  20815  emcllem6  20831  fsumharmonic  20842  ftalem2  20848  ftalem7  20853  basellem2  20856  basellem3  20857  basellem5  20859  basellem9  20863  ppiprm  20926  ppinprm  20927  chtprm  20928  chtnprm  20929  efchtdvds  20934  fsumdvdsmul  20972  chtublem  20987  fsumvma  20989  mersenne  21003  perfect  21007  dchrfi  21031  lgsne0  21109  lgseisenlem4  21128  lgsquadlem1  21130  2sqblem  21153  chebbnd2  21163  chto1lb  21164  rpvmasumlem  21173  dchrisumlem2  21176  dchrvmasumiflem1  21187  dchrvmasumiflem2  21188  dchrisum0fno1  21197  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  dchrmusumlem  21208  dchrvmasumlem  21209  rpvmasum  21212  rplogsum  21213  mudivsum  21216  mulog2sumlem3  21222  2vmadivsumlem  21226  selberglem2  21232  selberg2lem  21236  logdivbnd  21242  selberg3lem1  21243  selberg4lem1  21246  selberg4  21247  pntrsumo1  21251  selberg3r  21255  selberg4r  21256  selberg34r  21257  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntpbnd2  21273  pntlemo  21293  iseupa  21679  ablomul  21935  ghgrp  21948  rngoablo2  22002  vcoprne  22050  nvi  22085  ipval2lem3  22193  ipval2lem6  22199  ipf  22204  ubthlem1  22364  minvecolem2  22369  minvecolem4a  22371  hhshsslem2  22760  shsel1  22815  pjoccl  22927  5oalem1  23148  5oalem5  23152  3oalem2  23157  pjrni  23196  hmopd  23517  imaelshi  23553  adjbdlnb  23579  adjsslnop  23582  bracnlnval  23609  hmopidmchi  23646  disjabrex  24016  disjabrexf  24017  xrge0tsmsd  24215  subofld  24237  metideq  24280  lmxrge0  24329  indf1ofs  24415  esumf1o  24437  esumfsup  24452  esumpcvgval  24460  esumcvg  24468  unelsiga  24509  cldssbrsiga  24533  sxbrsigalem1  24627  ballotlemsf1o  24763  ballotlemrinv0  24782  eldmgm  24798  dmgmaddnn0  24803  lgamgulmlem2  24806  lgamcvg2  24831  regamcl  24837  relgamcl  24838  rpgamcl  24839  erdszelem8  24876  pconcon  24910  ptpcon  24912  txsconlem  24919  rescon  24925  cvmscld  24952  cvmliftmolem1  24960  cvmliftlem1  24964  cvmliftlem8  24971  cvmlift2lem9  24990  circum  25103  prodmolem2a  25252  fprodf1o  25264  fprodshft  25292  setlikespec  25454  wfrlem15  25544  onsuctop  26175  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  mbfresfi  26243  mbfposadd  26244  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  itgaddnclem2  26254  itgaddnc  26255  iblsubnc  26256  itgmulc2nclem2  26262  itgmulc2nc  26263  itgabsnc  26264  bddiblnc  26265  ftc1cnnclem  26268  ftc1anclem1  26270  ftc1anclem2  26271  ftc1anclem4  26273  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  ftc2nc  26279  areacirclem4  26284  isfne4  26340  islocfin  26367  fnejoin2  26389  unirep  26405  sdclem2  26437  geomcau  26456  ssbnd  26488  prdsbnd2  26495  divrngcl  26564  1idl  26627  inidl  26631  prnc  26668  ispridlc  26671  elrfi  26739  mzpaddmpt  26789  mzpmulmpt  26790  diophun  26823  elpell1qr2  26926  pellfundglb  26939  qirropth  26962  rmspecfund  26963  rmbaserp  26973  rmxnn  27007  jm2.27a  27067  jm2.27c  27069  fnwe2lem3  27118  lnmfg  27148  kercvrlsm  27149  lnmepi  27151  pwssplit4  27159  frlmgsum  27200  uvcresum  27210  frlmsplit2  27211  frlmup1  27218  hbtlem5  27300  hbt  27302  rngunsnply  27346  symggen  27379  psgnunilem1  27384  psgnunilem3  27387  acsfn1p  27475  rfcnpre1  27657  refsumcn  27668  rfcnpre2  27669  rfcnpre3  27671  rfcnpre4  27672  refsum2cnlem1  27675  mulc1cncfg  27688  stoweidlem9  27725  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem23  27739  stoweidlem31  27747  stoweidlem41  27757  stoweidlem47  27763  stirlinglem3  27792  stirlinglem7  27796  stirlinglem8  27797  sigardiv  27818  afvelrn  27999  bnj1145  29299  lkrlsp  29837  glbconN  30111  cvratlem  30155  llncvrlpln  30292  lplncvrlvol  30350  psubclsubN  30674  psubclinN  30682  4atexlemcnd  30806  cdleme23b  31084  cdlemk35  31646  dvaabl  31759  dia1elN  31789  diaintclN  31793  diasslssN  31794  dia2dimlem7  31805  dvadiaN  31863  dibintclN  31902  dihopelvalcpre  31983  dihsslss  32011  dih0rn  32019  dih1rn  32022  dihintcl  32079  dihmeetcl  32080  dochocss  32101  dochoccl  32104  dochsat  32118  dihsmsprn  32165  dochsnshp  32188  dochexmidlem6  32200  lcfl8b  32239  lclkrlem2g  32248  mapdpglem5N  32412  mapdpglem9  32415  mapdpglem14  32420  mapdpglem30a  32430  mapdpglem30b  32431  baerlem5amN  32451  baerlem5bmN  32452  baerlem5abmN  32453  mapdindp0  32454  mapdheq4lem  32466  mapdheq4  32467  mapdh6lem1N  32468  mapdh6lem2N  32469  mapdh7eN  32483  mapdh7cN  32484  mapdh7fN  32486  mapdh75e  32487  mapdh75fN  32490  mapdh8aa  32511  mapdh8d0N  32517  mapdh8d  32518  hdmap1eq2  32541  hdmap1eq4N  32542  hdmap1l6lem1  32543  hdmap1l6lem2  32544  hdmap1neglem1N  32563  hdmaprnlem7N  32593  hdmaprnlem17N  32601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator