MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtrd Structured version   Visualization version   GIF version

Theorem eleqtrd 2892
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrd.1 (𝜑𝐴𝐵)
eleqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eleqtrd (𝜑𝐴𝐶)

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eleq2d 2875 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 235 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870
This theorem is referenced by:  eleqtrrd  2893  eleqtrid  2896  eleqtrdi  2900  3eltr3d  2904  prel12g  4754  opth1  5332  0nelop  5351  fvelimad  6707  fviss  6716  tfisi  7553  fnwelem  7808  wfrlem17  7954  omeulem1  8191  oeeulem  8210  oeeui  8211  oaabs2  8255  omabs  8257  ercl  8283  erth  8321  ecelqsdm  8350  ordtypelem6  8971  ordtypelem7  8972  cantnfval  9115  cantnfp1lem3  9127  cantnflem4  9139  r1pwss  9197  rankonidlem  9241  rankxplim3  9294  fseqenlem2  9436  iunfictbso  9525  dfac12lem1  9554  dfac12lem2  9555  fin23lem30  9753  iundom2g  9951  fpwwe2lem6  10046  fpwwe2lem9  10049  lincmb01cmp  12873  fzopth  12939  fzoaddel2  13088  fzosubel2  13092  fzocatel  13096  zpnn0elfzo1  13106  fzoend  13123  peano2fzor  13139  monoord2  13397  sermono  13398  expmulnbnd  13592  bcpasc  13677  hash1elsn  13728  swrdcl  13998  revcl  14114  revlen  14115  fsum0diag2  15130  isumsplit  15187  fprodser  15295  sadadd  15806  sadass  15810  smuval2  15821  smumul  15832  vdwapun  16300  vdwlem9  16315  ramub1lem1  16352  prdsbasfn  16736  prdsbasprj  16737  pwsplusgval  16755  pwsmulrval  16756  pwsvscafval  16759  xpsaddlem  16838  xpsvsca  16842  xpsle  16844  mreexmrid  16906  homfeqval  16959  comfval2  16965  comfeq  16968  comfeqval  16970  oppccomfpropd  16989  invco  17033  sectepi  17046  issubc3  17111  funcf2  17130  fthepi  17190  nat1st2nd  17213  homarcl2  17287  coapm  17323  setcmon  17339  setcepi  17340  setcsect  17341  setcinv  17342  setciso  17343  catccatid  17354  resscatc  17357  catciso  17359  catcoppccl  17360  catcfuccl  17361  xpccatid  17430  catcxpccl  17449  xpcpropd  17450  evlfcl  17464  curfpropd  17475  hofcl  17501  yonedalem3  17522  yonffthlem  17524  poslubdg  17751  grpidd  17873  gsumress  17884  ismndd  17925  mndpropd  17928  issubmnd  17930  submnd0  17932  imasmnd  17941  frmdelbas  18010  grpidd2  18133  pwsinvg  18204  imasgrp  18207  submmulg  18263  subginvcl  18280  subgcl  18281  subgsub  18283  subgmulg  18285  1nsgtrivd  18318  quseccl  18328  gaid2  18425  submod  18686  odsubdvds  18688  sylow1lem4  18718  sylow2alem2  18735  lsmdisj2  18800  subgdisj1  18809  pj1id  18817  efgsrel  18852  efgrelexlemb  18868  efgcpbl2  18875  frgpcpbl  18877  frgp0  18878  frgpeccl  18879  frgpadd  18881  frgpup3lem  18895  frgpnabllem1  18986  cycsubgcyg  19014  prdsgsum  19094  dprdfeq0  19137  dmdprdsplitlem  19152  dpjidcl  19173  pgpfac1lem3a  19191  pgpfac1lem4  19193  pgpfaclem1  19196  pgpfaclem2  19197  ablfaclem2  19201  simpgnsgeqd  19216  simpgnsgbid  19218  ablsimpnosubgd  19219  ringidss  19323  ringpropd  19328  imasring  19365  qusring2  19366  kerf1ghm  19491  subrg1  19538  subrgmcl  19540  subrgdv  19545  subrgunit  19546  issubdrg  19553  resrhm  19557  lmodprop2d  19689  0lmhm  19805  lmhmpropd  19838  lspfixed  19893  lssacsex  19909  lbsextlem4  19926  quscrng  20006  znf1o  20243  psgnghm2  20270  elocv  20357  pjff  20401  frlmlss  20440  frlmsubgval  20454  frlmvscafval  20455  frlmvscavalb  20459  frlmvplusgscavalb  20460  frlmphl  20470  uvcresum  20482  frlmssuvc1  20483  frlmssuvc2  20484  frlmsslsp  20485  frlmup1  20487  assapropd  20558  psrelbas  20617  resspsrvsca  20656  subrgpsr  20657  mplcoe1  20705  mplbas2  20710  mplascl  20735  mplmon2cl  20739  mplmon2mul  20740  evlrhm  20768  mpfconst  20773  mhpvscacl  20802  vr1cl2  20822  ply1lss  20825  ply1subrg  20826  psropprmul  20867  evl1vsd  20968  evl1expd  20969  evl1gsumadd  20982  evl1gsummon  20989  matring  21048  matassa  21049  mat1  21052  mattposcl  21058  mavmulass  21154  mdetunilem9  21225  matinv  21282  cpmadugsumlemF  21481  cpmadugsumfi  21482  cpmidgsum2  21484  elcls3  21688  mreclatdemoBAD  21701  neiptopnei  21737  resstps  21792  ordtrest2lem  21808  ordtrest2  21809  pnfnei  21825  mnfnei  21826  iscnp2  21844  iscnp4  21868  cnrest2r  21892  lmcls  21907  lmcld  21908  cnt0  21951  cnhaus  21959  isreg2  21982  connclo  22020  1stccnp  22067  loclly  22092  lly1stc  22101  locfincmp  22131  unisngl  22132  comppfsc  22137  kgencmp2  22151  llycmpkgen2  22155  kgen2ss  22160  kgencn3  22163  pttoponconst  22202  txcls  22209  txbasval  22211  dfac14lem  22222  ptcn  22232  ptrescn  22244  txtube  22245  txcmplem1  22246  txlm  22253  txkgen  22257  xkopjcn  22261  cnmptkp  22285  xkoinjcn  22292  qtopkgen  22315  imastps  22326  isr0  22342  r0cld  22343  pt1hmeo  22411  ptuncnv  22412  ptunhmeo  22413  filintn0  22466  trnei  22497  flimfil  22574  flimopn  22580  fbflim2  22582  cnpflf2  22605  flfcnp  22609  flfcnp2  22612  fclsopn  22619  fcfnei  22640  cnpfcf  22646  flfcntr  22648  alexsublem  22649  ptcmplem3  22659  ptcmplem4  22660  cnextfres1  22673  tmdcn2  22694  tmdgsum  22700  tmdgsum2  22701  efmndtmd  22706  symgtgp  22711  tgphaus  22722  tgpt1  22723  qustgplem  22726  prdstmdd  22729  prdstgpd  22730  haustsms  22741  tsmscls  22743  tsmsmhm  22751  tsmsadd  22752  tgptsmscls  22755  tsmssplit  22757  restutop  22843  utopreg  22858  ressusp  22871  ucncn  22891  xmetunirn  22944  ressprdsds  22978  xpsdsval  22988  xblss2ps  23008  blbas  23037  mopntopon  23046  isxms2  23055  imasf1oxms  23096  imasf1oms  23097  prdsxmslem2  23136  tmsxpsval  23145  tngngp2  23258  tngngp  23260  tgioo  23401  metdseq0  23459  cncfmpt2f  23520  cncfcnvcn  23530  cnmptre  23532  cnheibor  23560  nmhmcn  23725  cvsdiv  23737  cvsdivcl  23738  cphsubrglem  23782  cphreccllem  23783  iscmet3  23897  relcmpcmet  23922  bcthlem4  23931  rrxds  23997  rrxvsca  23998  rrxplusgvscavalb  23999  rrxbasefi  24014  rrxmetfi  24016  minveclem4  24036  ivthicc  24062  evthicc  24063  ovolicc2lem4  24124  ovolicc2lem5  24125  iunmbl2  24161  vitalilem3  24214  cncombf  24262  cnmbf  24263  dvres2lem  24513  cpncn  24539  cpnres  24540  dvaddbr  24541  dvmulbr  24542  dvcobr  24549  dvcjbr  24552  dvrec  24558  dvcnvlem  24579  dvlip2  24598  dvivth  24613  lhop2  24618  lhop  24619  dvcnvrelem1  24620  dvcnvrelem2  24621  dvcnvre  24622  ftc1lem6  24644  mdegvscale  24676  mdegvsca  24677  fta1blem  24769  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  tayl0  24957  taylthlem1  24968  taylthlem2  24969  ulmdvlem3  24997  psercnlem2  25019  psercn  25021  efsubm  25143  cxpcn3  25337  loglesqrt  25347  efrlim  25555  ppinprm  25737  chtnprm  25739  dchrptlem1  25848  dchrptlem2  25849  tgbtwnouttr2  26289  tgldim0eq  26297  tgifscgr  26302  iscgrglt  26308  ercgrg  26311  tgcgrxfr  26312  motcgrg  26338  tglngne  26344  tgcolg  26348  tgbtwnconn1lem2  26367  tgbtwnconn1lem3  26368  legtri3  26384  legbtwn  26388  ncolne1  26419  tgisline  26421  tglinethru  26430  coltr3  26442  colline  26443  tglowdim2ln  26445  mirinv  26460  miriso  26464  mirauto  26478  miduniq  26479  krippenlem  26484  midexlem  26486  ragperp  26511  footexALT  26512  footexlem2  26514  perpdragALT  26521  perpdrag  26522  colperpexlem1  26524  colperpexlem3  26526  mideulem2  26528  midex  26531  opphllem1  26541  opphllem3  26543  opphllem4  26544  hlpasch  26550  trgcopy  26598  f1otrg  26665  axlowdimlem16  26751  elntg  26778  eengtrkg  26780  eengtrkge  26781  clwwlkccatlem  27774  grpoidinv2  28298  grpoinv  28308  ubthlem2  28654  shuni  29083  acunirnmpt  30422  acunirnmpt2  30423  acunirnmpt2f  30424  fpwrelmap  30495  fzm1ne1  30538  fzom1ne1  30550  ccatf1  30651  swrdf1  30656  gsummpt2d  30734  gsumhashmul  30741  odpmco  30780  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  tocyc01  30810  trsp2cyc  30815  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem1  30818  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cycpmconjv  30834  cycpmrn  30835  tocyccntz  30836  rngurd  30907  freshmansdream  30909  pidlnz  30991  elrspunidl  31014  qsidomlem1  31036  idlsrg0g  31059  srasubrg  31077  drgextlsp  31084  matdim  31101  lbslsat  31102  lindsunlem  31108  lbsdiflsp0  31110  dimkerim  31111  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  fldexttr  31136  extdgmul  31139  extdg1id  31141  rspectopn  31220  zarclsiin  31224  zarmxt1  31233  rspectps  31236  rhmpreimacn  31238  ordtrest2NEWlem  31275  ordtrest2NEW  31276  lmxrge0  31305  nmmulg  31319  rrhcn  31348  esumadd  31426  esumaddf  31430  esumcocn  31449  measiuns  31586  mbfmco2  31633  dya2iocnrect  31649  omscl  31663  omsf  31664  oms0  31665  sibf0  31702  sibfof  31708  sitgaddlemb  31716  fibp1  31769  ccatmulgnn0dir  31922  cxpcncf1  31976  ftc2re  31979  fsum2dsub  31988  reprf  31993  reprsum  31994  bnj1450  32432  bnj1501  32449  revpfxsfxrev  32472  indispconn  32591  connpconn  32592  pconnpi1  32594  sconnpi1  32596  cvmsss2  32631  cvmliftmolem1  32638  cvmliftlem8  32649  cvmliftlem10  32651  cvmliftlem11  32652  cvmlift2lem9  32668  cvmlift2lem12  32671  cvmlift3lem7  32682  mrsubcv  32867  mrsubff  32869  mrsubccat  32875  elmrsubrn  32877  mrsubco  32878  mrsubvrs  32879  frrlem8  33240  frrlem10  33242  nodenselem5  33302  linethru  33724  ivthALT  33793  neibastop2  33819  filnetlem4  33839  matunitlindflem2  35051  poimirlem1  35055  poimirlem2  35056  poimirlem8  35062  poimirlem9  35063  poimirlem16  35070  poimirlem17  35071  poimirlem19  35073  poimirlem20  35074  poimirlem22  35076  poimirlem23  35077  poimir  35087  broucube  35088  areacirclem4  35145  fdc  35180  isbnd3  35219  prdsbnd  35228  prdstotbnd  35229  prdsbnd2  35230  rrnequiv  35270  reheibor  35274  iscringd  35433  isfldidl  35503  eqvrelth  36003  eqlkr  36392  ldualvsubval  36450  dvalveclem  38318  dia2dimlem5  38361  dia2dimlem9  38365  tendoinvcl  38397  dvhgrp  38400  dvhlveclem  38401  dihpN  38629  dochsnkr2cl  38767  lcfl7lem  38792  lclkr  38826  lclkrs  38832  lcfrvalsnN  38834  lcfrlem4  38838  lcfrlem6  38840  lcfrlem16  38851  lcdvsubval  38911  lcdlkreqN  38915  mapdcl2  38949  mapdincl  38954  mapdlsmcl  38956  mapdpglem3  38968  hdmaprnlem9N  39150  hdmaplkr  39206  hdmapip0  39208  hdmapglem7a  39220  fltnltalem  39613  diophin  39708  acongeq  39919  isnumbasgrplem2  40043  proot1mul  40138  iunrelexpuztr  40415  ntrclsiex  40751  ntrneiiex  40774  ntrneinex  40775  elnelneqd  40903  grurankcld  40936  bccbc  41044  suctrALT  41527  restuni3  41748  disjf1o  41813  disjinfi  41815  choicefi  41824  fsneq  41830  fsneqrn  41835  unirnmapsn  41838  iunmapsn  41841  monoords  41924  elfzolem1  41948  uzfissfz  41953  monoord2xrv  42118  evthiccabs  42128  iooabslt  42131  tgqioo2  42179  islptre  42256  limciccioolb  42258  sumnnodd  42267  limcicciooub  42274  lptre2pt  42277  limcresiooub  42279  limcresioolb  42280  lptioo1cn  42283  reclimc  42290  liminfvalxr  42420  liminfvaluz  42429  limsupvaluz3  42435  fsumcncf  42515  ioccncflimc  42522  cncfuni  42523  icccncfext  42524  cncficcgt0  42525  icocncflimc  42526  cncfdmsn  42527  cncfiooicclem1  42530  cncfiooicc  42531  cncfioobd  42534  cxpcncf2  42536  fprodsub2cncf  42542  fprodadd2cncf  42543  fperdvper  42556  dvcosax  42563  dvnmul  42580  dvnprodlem1  42583  dvnprodlem2  42584  itgsubsticclem  42612  fvvolioof  42626  fvvolicof  42628  stoweidlem26  42663  stoweidlem27  42664  stoweidlem31  42668  stoweidlem34  42671  dirkercncflem2  42741  dirkercncflem3  42742  dirkercncflem4  42743  dirkercncf  42744  fourierdlem16  42760  fourierdlem20  42764  fourierdlem21  42765  fourierdlem22  42766  fourierdlem26  42770  fourierdlem32  42776  fourierdlem33  42777  fourierdlem38  42782  fourierdlem39  42783  fourierdlem46  42789  fourierdlem48  42791  fourierdlem49  42792  fourierdlem53  42796  fourierdlem60  42803  fourierdlem61  42804  fourierdlem69  42812  fourierdlem70  42813  fourierdlem71  42814  fourierdlem73  42816  fourierdlem74  42817  fourierdlem75  42818  fourierdlem76  42819  fourierdlem80  42823  fourierdlem81  42824  fourierdlem82  42825  fourierdlem83  42826  fourierdlem84  42827  fourierdlem85  42828  fourierdlem88  42831  fourierdlem89  42832  fourierdlem91  42834  fourierdlem92  42835  fourierdlem93  42836  fourierdlem100  42843  fourierdlem101  42844  fourierdlem103  42846  fourierdlem104  42847  fourierdlem107  42850  fourierdlem111  42854  fourierdlem112  42855  fourierdlem113  42856  fouriersw  42868  fouriercn  42869  etransclem24  42895  etransclem26  42897  etransclem28  42899  etransclem31  42902  etransclem32  42903  etransclem33  42904  etransclem34  42905  etransclem35  42906  etransclem38  42909  rrxtopnfi  42924  rrxtoponfi  42928  qndenserrnbl  42932  qndenserrnopnlem  42934  qndenserrn  42936  rrnprjdstle  42938  ioorrnopnlem  42941  prsal  42955  intsaluni  42964  salgencntex  42978  subsaliuncllem  42992  fge0iccico  43004  sge0sn  43013  sge0tsms  43014  sge0cl  43015  sge0f1o  43016  sge0pr  43028  sge0isum  43061  nnfoctbdjlem  43089  iundjiunlem  43093  iundjiun  43094  meadjiunlem  43099  psmeasure  43105  meaiininclem  43120  caragenelss  43135  omeunile  43139  carageniuncllem1  43155  carageniuncllem2  43156  0ome  43163  isomenndlem  43164  isomennd  43165  hoicvr  43182  ovnpnfelsup  43193  ovncvrrp  43198  ovnsubaddlem1  43204  hoidmv1le  43228  hoidmvlelem2  43230  hoidmvlelem3  43231  hoidmvlelem4  43232  hoidmvle  43234  ovnhoilem1  43235  hoi2toco  43241  ovncvr2  43245  hspdifhsp  43250  voncmpl  43255  hoiqssbl  43259  hspmbllem2  43261  hspmbl  43263  hoimbllem  43264  opnvonmbllem2  43267  mblvon  43273  ovolval3  43281  ovolval4lem1  43283  ovnovollem1  43290  ovnovollem2  43291  vonsn  43325  issmflem  43356  sssmf  43367  issmflelem  43373  issmfgtlem  43384  issmfgt  43385  smfaddlem1  43391  issmfgelem  43397  smflimlem3  43401  smfmullem2  43419  smfmullem4  43421  smfsuplem1  43437  smfsupmpt  43441  smfinfmpt  43445  smflimsuplem2  43447  smflimsuplem4  43449  smflimsupmpt  43455  smfliminfmpt  43458  fzoopth  43879  issubmgm2  44405  zlmodzxzel  44752  ply1mulgsum  44793
  Copyright terms: Public domain W3C validator