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

Theorem eleqtrd 2690
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 2673 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 221 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  eleqtrrd  2691  syl5eleq  2694  syl6eleq  2698  3eltr3d  2702  opth1  4870  0nelop  4886  fviss  6166  tfisi  6950  fnwelem  7179  wfrlem17  7318  omeulem1  7549  oeeulem  7568  oeeui  7569  oaabs2  7612  omabs  7614  ercl  7640  erth  7678  ecelqsdm  7704  ordtypelem6  8311  ordtypelem7  8312  cantnfval  8448  cantnfp1lem3  8460  cantnflem4  8472  r1pwss  8530  rankonidlem  8574  rankxplim3  8627  fseqenlem2  8731  iunfictbso  8820  dfac12lem1  8848  dfac12lem2  8849  fin23lem30  9047  iundom2g  9241  fpwwe2lem6  9336  fpwwe2lem9  9339  lincmb01cmp  12186  fzopth  12249  fzoaddel2  12391  fzosubel2  12395  fzocatel  12399  zpnn0elfzo1  12408  fzoend  12425  peano2fzor  12441  monoord2  12694  sermono  12695  expmulnbnd  12858  bcpasc  12970  swrdcl  13271  revcl  13361  revlen  13362  fsum0diag2  14357  isumsplit  14411  fprodser  14518  sadadd  15027  sadass  15031  smuval2  15042  smumul  15053  vdwapun  15516  vdwlem9  15531  ramub1lem1  15568  prdsbasfn  15954  prdsbasprj  15955  pwsplusgval  15973  pwsmulrval  15974  pwsvscafval  15977  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  mreexmrid  16126  homfeqval  16180  comfval2  16186  comfeq  16189  comfeqval  16191  oppccomfpropd  16210  invco  16254  sectepi  16267  issubc3  16332  funcf2  16351  funciso  16357  fthepi  16411  nat1st2nd  16434  fuciso  16458  homarcl2  16508  coapm  16544  setcmon  16560  setcepi  16561  setcsect  16562  setcinv  16563  setciso  16564  catccatid  16575  resscatc  16578  catciso  16580  catcoppccl  16581  catcfuccl  16582  xpccatid  16651  catcxpccl  16670  xpcpropd  16671  evlfcl  16685  curfpropd  16696  hofcl  16722  yonedalem3  16743  yonffthlem  16745  poslubdg  16972  grpidd  17091  gsumress  17099  ismndd  17136  mndpropd  17139  issubmnd  17141  submnd0  17143  imasmnd  17151  frmdelbas  17213  grpidd2  17282  pwsinvg  17351  imasgrp  17354  submmulg  17409  subginvcl  17426  subgcl  17427  subgsub  17429  subgmulg  17431  quseccl  17473  gaid2  17559  submod  17807  odsubdvds  17809  sylow1lem4  17839  sylow2alem2  17856  lsmdisj2  17918  subgdisj1  17927  pj1id  17935  efgsrel  17970  efgrelexlemb  17986  efgcpbl2  17993  frgpcpbl  17995  frgp0  17996  frgpeccl  17997  frgpadd  17999  frgpup3lem  18013  frgpnabllem1  18099  cycsubgcyg  18125  prdsgsum  18200  dprdfeq0  18244  dmdprdsplitlem  18259  dpjidcl  18280  pgpfac1lem3a  18298  pgpfac1lem4  18300  pgpfaclem1  18303  pgpfaclem2  18304  ablfaclem2  18308  ringidss  18400  ringpropd  18405  imasring  18442  qusring2  18443  kerf1hrm  18566  subrg1  18613  subrgmcl  18615  subrgdv  18620  subrgunit  18621  issubdrg  18628  resrhm  18632  lmodprop2d  18748  0lmhm  18861  lmhmpropd  18894  lspfixed  18949  lssacsex  18965  lbsextlem4  18982  quscrng  19061  assapropd  19148  psrelbas  19200  resspsrvsca  19239  subrgpsr  19240  mplcoe1  19286  mplbas2  19291  mplascl  19317  mplmon2cl  19321  mplmon2mul  19322  evlrhm  19346  mpfconst  19351  vr1cl2  19384  ply1lss  19387  ply1subrg  19388  psropprmul  19429  evl1vsd  19529  evl1expd  19530  evl1gsumadd  19543  evl1gsummon  19550  znf1o  19719  psgnghm2  19746  elocv  19831  pjff  19875  frlmlss  19914  frlmsubgval  19927  frlmvscafval  19928  frlmphl  19939  uvcresum  19951  frlmssuvc1  19952  frlmssuvc2  19953  frlmsslsp  19954  frlmup1  19956  matring  20068  matassa  20069  mat1  20072  mattposcl  20078  mavmulass  20174  mdetunilem9  20245  matinv  20302  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmidgsum2  20503  elcls3  20697  mreclatdemoBAD  20710  neiptopnei  20746  resstps  20801  ordtrest2lem  20817  ordtrest2  20818  pnfnei  20834  mnfnei  20835  iscnp2  20853  iscnp4  20877  cnrest2r  20901  lmcls  20916  lmcld  20917  cnt0  20960  cnhaus  20968  isreg2  20991  conclo  21028  1stccnp  21075  loclly  21100  lly1stc  21109  locfincmp  21139  unisngl  21140  comppfsc  21145  kgencmp2  21159  llycmpkgen2  21163  kgen2ss  21168  kgencn3  21171  pttoponconst  21210  txcls  21217  txbasval  21219  dfac14lem  21230  ptcn  21240  ptrescn  21252  txtube  21253  txcmplem1  21254  txlm  21261  txkgen  21265  xkopjcn  21269  cnmptkp  21293  xkoinjcn  21300  qtopkgen  21323  imastps  21334  isr0  21350  r0cld  21351  pt1hmeo  21419  ptuncnv  21420  ptunhmeo  21421  filintn0  21475  trnei  21506  flimfil  21583  flimopn  21589  fbflim2  21591  cnpflf2  21614  flfcnp  21618  flfcnp2  21621  fclsopn  21628  fcfnei  21649  cnpfcf  21655  flfcntr  21657  alexsublem  21658  ptcmplem3  21668  ptcmplem4  21669  cnextfres1  21682  tmdcn2  21703  tmdgsum  21709  tmdgsum2  21710  symgtgp  21715  tgphaus  21730  tgpt1  21731  qustgplem  21734  prdstmdd  21737  prdstgpd  21738  haustsms  21749  tsmscls  21751  tsmsmhm  21759  tsmsadd  21760  tgptsmscls  21763  tsmssplit  21765  restutop  21851  utopreg  21866  ressusp  21879  ucncn  21899  xmetunirn  21952  ressprdsds  21986  xpsdsval  21996  xblss2ps  22016  blbas  22045  mopntopon  22054  isxms2  22063  imasf1oxms  22104  imasf1oms  22105  prdsxmslem2  22144  tmsxpsval  22153  tngngp2  22266  tngngp  22268  tgioo  22407  metdseq0  22465  cncfmpt2f  22525  cncfcnvcn  22532  cnmptre  22534  cnheibor  22562  nmhmcn  22728  cvsdiv  22740  cvsdivcl  22741  cphsubrglem  22785  cphreccllem  22786  iscmet3  22899  relcmpcmet  22923  bcthlem4  22932  rrxds  22989  minveclem4  23011  ivthicc  23034  evthicc  23035  ovolicc2lem4  23095  ovolicc2lem5  23096  iunmbl2  23132  vitalilem3  23185  cncombf  23231  cnmbf  23232  dvres2lem  23480  cpncn  23505  cpnres  23506  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvcnvlem  23543  dvlip2  23562  dvivth  23577  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  ftc1lem6  23608  mdegvscale  23639  mdegvsca  23640  fta1blem  23732  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  tayl0  23920  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  psercnlem2  23982  psercn  23984  efsubm  24101  cxpcn3  24289  loglesqrt  24299  efrlim  24496  ppinprm  24678  chtnprm  24680  dchrptlem1  24789  dchrptlem2  24790  tgbtwnouttr2  25190  tgldim0eq  25198  tgifscgr  25203  iscgrglt  25209  ercgrg  25212  tgcgrxfr  25213  motcgrg  25239  tglngne  25245  tgcolg  25249  tgbtwnconn1lem2  25268  tgbtwnconn1lem3  25269  legtri3  25285  legbtwn  25289  ncolne1  25320  tgisline  25322  tglinethru  25331  coltr3  25343  colline  25344  tglowdim2ln  25346  mirinv  25361  miriso  25365  mirauto  25379  miduniq  25380  krippenlem  25385  midexlem  25387  ragperp  25412  footex  25413  perpdragALT  25419  perpdrag  25420  colperpexlem1  25422  colperpexlem3  25424  mideulem2  25426  midex  25429  opphllem1  25439  opphllem3  25441  opphllem4  25442  hlpasch  25448  trgcopy  25496  acopyeu  25525  f1otrg  25551  axlowdimlem16  25637  elntg  25664  eengtrkg  25665  eengtrkge  25666  eupap1  26503  grpoidinv2  26753  grpoinv  26763  ubthlem2  27111  shuni  27543  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  fpwrelmap  28896  gsummpt2d  29112  rngurd  29119  ordtrest2NEWlem  29296  ordtrest2NEW  29297  lmxrge0  29326  nmmulg  29340  rrhcn  29369  esumadd  29446  esumaddf  29450  esumcocn  29469  measiuns  29607  mbfmco2  29654  dya2iocnrect  29670  omscl  29684  omsf  29685  oms0  29686  sibf0  29723  sibfof  29729  sitgaddlemb  29737  fibp1  29790  ccatmulgnn0dir  29945  bnj1450  30372  bnj1501  30389  indispcon  30470  conpcon  30471  pconpi1  30473  sconpi1  30475  cvmsss2  30510  cvmliftmolem1  30517  cvmliftlem8  30528  cvmliftlem10  30530  cvmliftlem11  30531  cvmlift2lem9  30547  cvmlift2lem12  30550  cvmlift3lem7  30561  mrsubcv  30661  mrsubff  30663  mrsubccat  30669  elmrsubrn  30671  mrsubco  30672  mrsubvrs  30673  linethru  31430  ivthALT  31500  neibastop2  31526  filnetlem4  31546  matunitlindflem2  32576  poimirlem1  32580  poimirlem2  32581  poimirlem8  32587  poimirlem9  32588  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimir  32612  broucube  32613  areacirclem4  32673  fdc  32711  isbnd3  32753  prdsbnd  32762  prdstotbnd  32763  prdsbnd2  32764  rrnequiv  32804  reheibor  32808  iscringd  32967  isfldidl  33037  eqlkr  33404  ldualvsubval  33462  dvalveclem  35332  dia2dimlem5  35375  dia2dimlem9  35379  tendoinvcl  35411  dvhgrp  35414  dvhlveclem  35415  dihpN  35643  dochsnkr2cl  35781  lcfl7lem  35806  lclkr  35840  lclkrs  35846  lcfrvalsnN  35848  lcfrlem4  35852  lcfrlem6  35854  lcfrlem16  35865  lcdvsubval  35925  lcdlkreqN  35929  mapdcl2  35963  mapdincl  35968  mapdlsmcl  35970  mapdpglem3  35982  hdmaprnlem9N  36167  hdmaplkr  36223  hdmapip0  36225  hdmapglem7a  36237  diophin  36354  acongeq  36568  isnumbasgrplem2  36693  proot1mul  36796  iunrelexpuztr  37030  ntrclsiex  37371  ntrneiiex  37394  ntrneinex  37395  bccbc  37566  suctrALT  38083  restuni3  38333  disjf1o  38373  disjinfi  38375  choicefi  38387  fsneq  38393  fsneqrn  38398  unirnmapsn  38401  iunmapsn  38404  monoords  38452  elfzolem1  38478  uzfissfz  38483  evthiccabs  38565  iooabslt  38568  tgqioo2  38621  islptre  38686  limciccioolb  38688  sumnnodd  38697  limcicciooub  38704  lptre2pt  38707  limcresiooub  38709  limcresioolb  38710  lptioo1cn  38713  reclimc  38720  fsumcncf  38763  ioccncflimc  38771  cncfuni  38772  icccncfext  38773  cncficcgt0  38774  icocncflimc  38775  cncfdmsn  38776  cncfiooicclem1  38779  cncfiooicc  38780  cncfioobd  38783  cxpcncf2  38786  fprodsub2cncf  38792  fprodadd2cncf  38793  fperdvper  38808  dvcosax  38816  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  itgsubsticclem  38867  fvvolioof  38882  fvvolicof  38884  stoweidlem26  38919  stoweidlem27  38920  stoweidlem31  38924  stoweidlem34  38927  dirkercncflem2  38997  dirkercncflem3  38998  dirkercncflem4  38999  dirkercncf  39000  fourierdlem16  39016  fourierdlem20  39020  fourierdlem21  39021  fourierdlem22  39022  fourierdlem26  39026  fourierdlem32  39032  fourierdlem33  39033  fourierdlem38  39038  fourierdlem39  39039  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem53  39052  fourierdlem60  39059  fourierdlem61  39060  fourierdlem69  39068  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem100  39099  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fouriersw  39124  fouriercn  39125  etransclem24  39151  etransclem26  39153  etransclem28  39155  etransclem31  39158  etransclem32  39159  etransclem33  39160  etransclem34  39161  etransclem35  39162  etransclem38  39165  rrxbasefi  39179  rrxdsfi  39181  rrxtopnfi  39182  rrxmetfi  39183  rrxtoponfi  39187  qndenserrnbl  39191  qndenserrnopnlem  39193  qndenserrn  39195  rrnprjdstle  39197  ioorrnopnlem  39200  prsal  39214  intsaluni  39223  salgencntex  39237  subsaliuncllem  39251  fge0iccico  39263  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0pr  39287  sge0isum  39320  nnfoctbdjlem  39348  iundjiunlem  39352  iundjiun  39353  meadjiunlem  39358  psmeasure  39364  meaiininclem  39376  caragenelss  39391  omeunile  39395  carageniuncllem1  39411  carageniuncllem2  39412  0ome  39419  isomenndlem  39420  isomennd  39421  hoicvr  39438  ovnpnfelsup  39449  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmv1le  39484  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvle  39490  ovnhoilem1  39491  hoi2toco  39497  ovncvr2  39501  hspdifhsp  39506  voncmpl  39511  hoiqssbl  39515  hspmbllem2  39517  hspmbl  39519  hoimbllem  39520  opnvonmbllem2  39523  mblvon  39529  ovolval3  39537  ovolval4lem1  39539  ovnovollem1  39546  ovnovollem2  39547  vonval2  39559  vonsn  39582  issmflem  39613  sssmf  39625  issmflelem  39631  issmfgtlem  39642  issmfgt  39643  smfaddlem1  39649  issmfgelem  39655  smflimlem3  39659  smfmullem2  39677  smfmullem4  39679  fzoopth  40360  issubmgm2  41580  zlmodzxzel  41926  ply1mulgsum  41972
  Copyright terms: Public domain W3C validator