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

Theorem eleqtrd 2732
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 2716 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 222 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  eleqtrrd  2733  syl5eleq  2736  syl6eleq  2740  3eltr3d  2744  opth1  4973  0nelop  4989  fviss  6295  tfisi  7100  fnwelem  7337  wfrlem17  7476  omeulem1  7707  oeeulem  7726  oeeui  7727  oaabs2  7770  omabs  7772  ercl  7798  erth  7834  ecelqsdm  7860  ordtypelem6  8469  ordtypelem7  8470  cantnfval  8603  cantnfp1lem3  8615  cantnflem4  8627  r1pwss  8685  rankonidlem  8729  rankxplim3  8782  fseqenlem2  8886  iunfictbso  8975  dfac12lem1  9003  dfac12lem2  9004  fin23lem30  9202  iundom2g  9400  fpwwe2lem6  9495  fpwwe2lem9  9498  lincmb01cmp  12353  fzopth  12416  fzoaddel2  12563  fzosubel2  12567  fzocatel  12571  zpnn0elfzo1  12581  fzoend  12599  peano2fzor  12615  monoord2  12872  sermono  12873  expmulnbnd  13036  bcpasc  13148  swrdcl  13464  revcl  13556  revlen  13557  fsum0diag2  14559  isumsplit  14616  fprodser  14723  sadadd  15236  sadass  15240  smuval2  15251  smumul  15262  vdwapun  15725  vdwlem9  15740  ramub1lem1  15777  prdsbasfn  16178  prdsbasprj  16179  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  xpsaddlem  16282  xpsvsca  16286  xpsle  16288  mreexmrid  16350  homfeqval  16404  comfval2  16410  comfeq  16413  comfeqval  16415  oppccomfpropd  16434  invco  16478  sectepi  16491  issubc3  16556  funcf2  16575  funciso  16581  fthepi  16635  nat1st2nd  16658  fuciso  16682  homarcl2  16732  coapm  16768  setcmon  16784  setcepi  16785  setcsect  16786  setcinv  16787  setciso  16788  catccatid  16799  resscatc  16802  catciso  16804  catcoppccl  16805  catcfuccl  16806  xpccatid  16875  catcxpccl  16894  xpcpropd  16895  evlfcl  16909  curfpropd  16920  hofcl  16946  yonedalem3  16967  yonffthlem  16969  poslubdg  17196  grpidd  17315  gsumress  17323  ismndd  17360  mndpropd  17363  issubmnd  17365  submnd0  17367  imasmnd  17375  frmdelbas  17437  grpidd2  17506  pwsinvg  17575  imasgrp  17578  submmulg  17633  subginvcl  17650  subgcl  17651  subgsub  17653  subgmulg  17655  quseccl  17697  gaid2  17782  submod  18030  odsubdvds  18032  sylow1lem4  18062  sylow2alem2  18079  lsmdisj2  18141  subgdisj1  18150  pj1id  18158  efgsrel  18193  efgrelexlemb  18209  efgcpbl2  18216  frgpcpbl  18218  frgp0  18219  frgpeccl  18220  frgpadd  18222  frgpup3lem  18236  frgpnabllem1  18322  cycsubgcyg  18348  prdsgsum  18423  dprdfeq0  18467  dmdprdsplitlem  18482  dpjidcl  18503  pgpfac1lem3a  18521  pgpfac1lem4  18523  pgpfaclem1  18526  pgpfaclem2  18527  ablfaclem2  18531  ringidss  18623  ringpropd  18628  imasring  18665  qusring2  18666  kerf1hrm  18791  subrg1  18838  subrgmcl  18840  subrgdv  18845  subrgunit  18846  issubdrg  18853  resrhm  18857  lmodprop2d  18973  0lmhm  19088  lmhmpropd  19121  lspfixed  19176  lssacsex  19192  lbsextlem4  19209  quscrng  19288  assapropd  19375  psrelbas  19427  resspsrvsca  19466  subrgpsr  19467  mplcoe1  19513  mplbas2  19518  mplascl  19544  mplmon2cl  19548  mplmon2mul  19549  evlrhm  19573  mpfconst  19578  vr1cl2  19611  ply1lss  19614  ply1subrg  19615  psropprmul  19656  evl1vsd  19756  evl1expd  19757  evl1gsumadd  19770  evl1gsummon  19777  znf1o  19948  psgnghm2  19975  elocv  20060  pjff  20104  frlmlss  20143  frlmsubgval  20156  frlmvscafval  20157  frlmphl  20168  uvcresum  20180  frlmssuvc1  20181  frlmssuvc2  20182  frlmsslsp  20183  frlmup1  20185  matring  20297  matassa  20298  mat1  20301  mattposcl  20307  mavmulass  20403  mdetunilem9  20474  matinv  20531  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmidgsum2  20732  elcls3  20935  mreclatdemoBAD  20948  neiptopnei  20984  resstps  21039  ordtrest2lem  21055  ordtrest2  21056  pnfnei  21072  mnfnei  21073  iscnp2  21091  iscnp4  21115  cnrest2r  21139  lmcls  21154  lmcld  21155  cnt0  21198  cnhaus  21206  isreg2  21229  connclo  21266  1stccnp  21313  loclly  21338  lly1stc  21347  locfincmp  21377  unisngl  21378  comppfsc  21383  kgencmp2  21397  llycmpkgen2  21401  kgen2ss  21406  kgencn3  21409  pttoponconst  21448  txcls  21455  txbasval  21457  dfac14lem  21468  ptcn  21478  ptrescn  21490  txtube  21491  txcmplem1  21492  txlm  21499  txkgen  21503  xkopjcn  21507  cnmptkp  21531  xkoinjcn  21538  qtopkgen  21561  imastps  21572  isr0  21588  r0cld  21589  pt1hmeo  21657  ptuncnv  21658  ptunhmeo  21659  filintn0  21712  trnei  21743  flimfil  21820  flimopn  21826  fbflim2  21828  cnpflf2  21851  flfcnp  21855  flfcnp2  21858  fclsopn  21865  fcfnei  21886  cnpfcf  21892  flfcntr  21894  alexsublem  21895  ptcmplem3  21905  ptcmplem4  21906  cnextfres1  21919  tmdcn2  21940  tmdgsum  21946  tmdgsum2  21947  symgtgp  21952  tgphaus  21967  tgpt1  21968  qustgplem  21971  prdstmdd  21974  prdstgpd  21975  haustsms  21986  tsmscls  21988  tsmsmhm  21996  tsmsadd  21997  tgptsmscls  22000  tsmssplit  22002  restutop  22088  utopreg  22103  ressusp  22116  ucncn  22136  xmetunirn  22189  ressprdsds  22223  xpsdsval  22233  xblss2ps  22253  blbas  22282  mopntopon  22291  isxms2  22300  imasf1oxms  22341  imasf1oms  22342  prdsxmslem2  22381  tmsxpsval  22390  tngngp2  22503  tngngp  22505  tgioo  22646  metdseq0  22704  cncfmpt2f  22764  cncfcnvcn  22771  cnmptre  22773  cnheibor  22801  nmhmcn  22966  cvsdiv  22978  cvsdivcl  22979  cphsubrglem  23023  cphreccllem  23024  iscmet3  23137  relcmpcmet  23161  bcthlem4  23170  rrxds  23227  minveclem4  23249  ivthicc  23273  evthicc  23274  ovolicc2lem4  23334  ovolicc2lem5  23335  iunmbl2  23371  vitalilem3  23424  cncombf  23470  cnmbf  23471  dvres2lem  23719  cpncn  23744  cpnres  23745  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvcjbr  23757  dvrec  23763  dvcnvlem  23784  dvlip2  23803  dvivth  23818  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  ftc1lem6  23849  mdegvscale  23880  mdegvsca  23881  fta1blem  23973  plyaddlem1  24014  plymullem1  24015  coeeulem  24025  tayl0  24161  taylthlem1  24172  taylthlem2  24173  ulmdvlem3  24201  psercnlem2  24223  psercn  24225  efsubm  24342  cxpcn3  24534  loglesqrt  24544  efrlim  24741  ppinprm  24923  chtnprm  24925  dchrptlem1  25034  dchrptlem2  25035  tgbtwnouttr2  25435  tgldim0eq  25443  tgifscgr  25448  iscgrglt  25454  ercgrg  25457  tgcgrxfr  25458  motcgrg  25484  tglngne  25490  tgcolg  25494  tgbtwnconn1lem2  25513  tgbtwnconn1lem3  25514  legtri3  25530  legbtwn  25534  ncolne1  25565  tgisline  25567  tglinethru  25576  coltr3  25588  colline  25589  tglowdim2ln  25591  mirinv  25606  miriso  25610  mirauto  25624  miduniq  25625  krippenlem  25630  midexlem  25632  ragperp  25657  footex  25658  perpdragALT  25664  perpdrag  25665  colperpexlem1  25667  colperpexlem3  25669  mideulem2  25671  midex  25674  opphllem1  25684  opphllem3  25686  opphllem4  25687  hlpasch  25693  trgcopy  25741  acopyeu  25770  f1otrg  25796  axlowdimlem16  25882  elntg  25909  eengtrkg  25910  eengtrkge  25911  grpoidinv2  27497  grpoinv  27507  ubthlem2  27855  shuni  28287  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  fpwrelmap  29636  gsummpt2d  29909  rngurd  29916  ordtrest2NEWlem  30096  ordtrest2NEW  30097  lmxrge0  30126  nmmulg  30140  rrhcn  30169  esumadd  30247  esumaddf  30251  esumcocn  30270  measiuns  30408  mbfmco2  30455  dya2iocnrect  30471  omscl  30485  omsf  30486  oms0  30487  sibf0  30524  sibfof  30530  sitgaddlemb  30538  fibp1  30591  ccatmulgnn0dir  30747  cxpcncf1  30801  ftc2re  30804  fsum2dsub  30813  reprf  30818  reprsum  30819  bnj1450  31244  bnj1501  31261  indispconn  31342  connpconn  31343  pconnpi1  31345  sconnpi1  31347  cvmsss2  31382  cvmliftmolem1  31389  cvmliftlem8  31400  cvmliftlem10  31402  cvmliftlem11  31403  cvmlift2lem9  31419  cvmlift2lem12  31422  cvmlift3lem7  31433  mrsubcv  31533  mrsubff  31535  mrsubccat  31541  elmrsubrn  31543  mrsubco  31544  mrsubvrs  31545  nodenselem5  31963  linethru  32385  ivthALT  32455  neibastop2  32481  filnetlem4  32501  matunitlindflem2  33536  poimirlem1  33540  poimirlem2  33541  poimirlem8  33547  poimirlem9  33548  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimir  33572  broucube  33573  areacirclem4  33633  fdc  33671  isbnd3  33713  prdsbnd  33722  prdstotbnd  33723  prdsbnd2  33724  rrnequiv  33764  reheibor  33768  iscringd  33927  isfldidl  33997  eqlkr  34704  ldualvsubval  34762  dvalveclem  36631  dia2dimlem5  36674  dia2dimlem9  36678  tendoinvcl  36710  dvhgrp  36713  dvhlveclem  36714  dihpN  36942  dochsnkr2cl  37080  lcfl7lem  37105  lclkr  37139  lclkrs  37145  lcfrvalsnN  37147  lcfrlem4  37151  lcfrlem6  37153  lcfrlem16  37164  lcdvsubval  37224  lcdlkreqN  37228  mapdcl2  37262  mapdincl  37267  mapdlsmcl  37269  mapdpglem3  37281  hdmaprnlem9N  37466  hdmaplkr  37522  hdmapip0  37524  hdmapglem7a  37536  diophin  37653  acongeq  37867  isnumbasgrplem2  37991  proot1mul  38094  iunrelexpuztr  38328  ntrclsiex  38668  ntrneiiex  38691  ntrneinex  38692  bccbc  38861  suctrALT  39375  restuni3  39615  disjf1o  39692  disjinfi  39694  choicefi  39706  fsneq  39712  fsneqrn  39717  unirnmapsn  39720  iunmapsn  39723  fvelimad  39772  monoords  39825  elfzolem1  39850  uzfissfz  39855  monoord2xrv  40027  evthiccabs  40036  iooabslt  40039  tgqioo2  40092  islptre  40169  limciccioolb  40171  sumnnodd  40180  limcicciooub  40187  lptre2pt  40190  limcresiooub  40192  limcresioolb  40193  lptioo1cn  40196  reclimc  40203  liminfvalxr  40333  liminfvaluz  40342  limsupvaluz3  40348  fsumcncf  40409  ioccncflimc  40416  cncfuni  40417  icccncfext  40418  cncficcgt0  40419  icocncflimc  40420  cncfdmsn  40421  cncfiooicclem1  40424  cncfiooicc  40425  cncfioobd  40428  cxpcncf2  40431  fprodsub2cncf  40437  fprodadd2cncf  40438  fperdvper  40451  dvcosax  40459  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  itgsubsticclem  40509  fvvolioof  40524  fvvolicof  40526  stoweidlem26  40561  stoweidlem27  40562  stoweidlem31  40566  stoweidlem34  40569  dirkercncflem2  40639  dirkercncflem3  40640  dirkercncflem4  40641  dirkercncf  40642  fourierdlem16  40658  fourierdlem20  40662  fourierdlem21  40663  fourierdlem22  40664  fourierdlem26  40668  fourierdlem32  40674  fourierdlem33  40675  fourierdlem38  40680  fourierdlem39  40681  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem53  40694  fourierdlem60  40701  fourierdlem61  40702  fourierdlem69  40710  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem89  40730  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem100  40741  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fouriersw  40766  fouriercn  40767  etransclem24  40793  etransclem26  40795  etransclem28  40797  etransclem31  40800  etransclem32  40801  etransclem33  40802  etransclem34  40803  etransclem35  40804  etransclem38  40807  rrxbasefi  40821  rrxdsfi  40823  rrxtopnfi  40824  rrxmetfi  40825  rrxtoponfi  40829  qndenserrnbl  40833  qndenserrnopnlem  40835  qndenserrn  40837  rrnprjdstle  40839  ioorrnopnlem  40842  prsal  40856  intsaluni  40865  salgencntex  40879  subsaliuncllem  40893  fge0iccico  40905  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0pr  40929  sge0isum  40962  nnfoctbdjlem  40990  iundjiunlem  40994  iundjiun  40995  meadjiunlem  41000  psmeasure  41006  meaiininclem  41021  caragenelss  41036  omeunile  41040  carageniuncllem1  41056  carageniuncllem2  41057  0ome  41064  isomenndlem  41065  isomennd  41066  hoicvr  41083  ovnpnfelsup  41094  ovncvrrp  41099  ovnsubaddlem1  41105  hoidmv1le  41129  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvle  41135  ovnhoilem1  41136  hoi2toco  41142  ovncvr2  41146  hspdifhsp  41151  voncmpl  41156  hoiqssbl  41160  hspmbllem2  41162  hspmbl  41164  hoimbllem  41165  opnvonmbllem2  41168  mblvon  41174  ovolval3  41182  ovolval4lem1  41184  ovnovollem1  41191  ovnovollem2  41192  vonsn  41226  issmflem  41257  sssmf  41268  issmflelem  41274  issmfgtlem  41285  issmfgt  41286  smfaddlem1  41292  issmfgelem  41298  smflimlem3  41302  smfmullem2  41320  smfmullem4  41322  smfsuplem1  41338  smfsupmpt  41342  smfinfmpt  41346  smflimsuplem2  41348  smflimsuplem4  41350  smflimsupmpt  41356  smfliminfmpt  41359  fzoopth  41662  issubmgm2  42115  zlmodzxzel  42458  ply1mulgsum  42503
  Copyright terms: Public domain W3C validator