Theorem eleqtrd 2831

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

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2815	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 231	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806

This theorem is referenced by:  eleqtrrd  2832  eleqtrid  2835  eleqtrdi  2839  3eltr3d  2843  prel12g  4865  opth1  5477  0nelop  5498  fvelimad  6966  fviss  6975  feldmfvelcdm  7096  tfisi  7863  fnwelem  8136  frrlem8  8299  frrlem10  8301  fprresex  8316  wfrlem17OLD  8346  omeulem1  8603  oeeulem  8622  oeeui  8623  oaabs2  8670  omabs  8672  ercl  8736  erth  8775  ecelqsdm  8806  ordtypelem6  9547  ordtypelem7  9548  cantnfval  9692  cantnfp1lem3  9704  cantnflem4  9716  r1pwss  9808  rankonidlem  9852  rankxplim3  9905  fseqenlem2  10049  iunfictbso  10138  dfac12lem1  10167  dfac12lem2  10168  fin23lem30  10366  iundom2g  10564  fpwwe2lem5  10659  fpwwe2lem8  10662  lincmb01cmp  13505  fzopth  13571  fzoaddel2  13721  fzosubel2  13725  fzocatel  13729  zpnn0elfzo1  13739  fzoend  13756  peano2fzor  13772  monoord2  14031  sermono  14032  expmulnbnd  14230  bcpasc  14313  hash1elsn  14363  swrdcl  14628  revcl  14744  revlen  14745  fsum0diag2  15762  isumsplit  15819  fprodser  15926  sadadd  16442  sadass  16446  smuval2  16457  smumul  16468  vdwapun  16943  vdwlem9  16958  ramub1lem1  16995  prdsbasfn  17453  prdsbasprj  17454  pwsplusgval  17472  pwsmulrval  17473  pwsvscafval  17476  xpsaddlem  17555  xpsvsca  17559  xpsle  17561  mreexmrid  17623  homfeqval  17677  comfval2  17683  comfeq  17686  comfeqval  17688  oppccomfpropd  17709  invco  17754  sectepi  17767  issubc3  17835  funcf2  17854  fthepi  17917  nat1st2nd  17941  homarcl2  18024  coapm  18060  setcmon  18076  setcepi  18077  setcsect  18078  setcinv  18079  setciso  18080  cat1lem  18085  catccatid  18095  resscatc  18098  catciso  18100  catcbascl  18101  catcoppccl  18106  catcoppcclOLD  18107  catcfuccl  18108  catcfucclOLD  18109  xpccatid  18179  catcxpccl  18198  catcxpcclOLD  18199  xpcpropd  18200  evlfcl  18214  curfpropd  18225  hofcl  18251  yonedalem3  18272  yonffthlem  18274  poslubdg  18406  grpidd  18631  gsumress  18642  issubmgm2  18663  sgrppropd  18691  ismndd  18716  mndpropd  18719  issubmnd  18721  submnd0  18723  imasmnd  18732  xpsmnd0  18735  frmdelbas  18805  grpidd2  18934  pwsinvg  19009  imasgrp  19012  xpsinv  19016  xpsgrpsub  19017  submmulg  19073  subginvcl  19090  subgcl  19091  subgsub  19093  subgmulg  19095  1nsgtrivd  19129  quseccl0  19140  kerf1ghm  19201  ghmquskerlem1  19234  ghmquskerco  19235  ghmqusker  19238  gaid2  19254  finodsubmsubg  19522  submod  19524  odsubdvds  19526  sylow1lem4  19556  sylow2alem2  19573  lsmdisj2  19637  subgdisj1  19646  pj1id  19654  efgsrel  19689  efgrelexlemb  19705  efgcpbl2  19712  frgpcpbl  19714  frgp0  19715  frgpeccl  19716  frgpadd  19718  frgpup3lem  19732  frgpnabllem1  19828  cycsubgcyg  19856  prdsgsum  19936  dprdfeq0  19979  dmdprdsplitlem  19994  dpjidcl  20015  pgpfac1lem3a  20033  pgpfac1lem4  20035  pgpfaclem1  20038  pgpfaclem2  20039  ablfaclem2  20043  simpgnsgeqd  20058  simpgnsgbid  20060  ablsimpnosubgd  20061  rngpropd  20114  imasrng  20117  ringurd  20125  ringidss  20213  ringpropd  20224  imasring  20266  xpsring1d  20269  qusring2  20270  lringuplu  20481  subrngmcl  20494  subrg1  20521  subrgdv  20528  subrgunit  20529  resrhm  20540  issubdrg  20668  lmodprop2d  20807  0lmhm  20925  lmhmpropd  20958  lspfixed  21016  lssacsex  21032  lbsextlem4  21049  quscrng  21175  rngqiprngimf  21187  rngqiprngimfo  21191  rngqiprngfulem4  21204  znf1o  21485  freshmansdream  21508  psgnghm2  21513  elocv  21600  pjff  21646  frlmlss  21685  frlmsubgval  21699  frlmvscafval  21700  frlmvscavalb  21704  frlmvplusgscavalb  21705  frlmphl  21715  uvcresum  21727  frlmssuvc1  21728  frlmssuvc2  21729  frlmsslsp  21730  frlmup1  21732  sraassab  21801  assapropd  21805  psrelbas  21879  resspsrvsca  21920  subrgpsr  21921  mplcoe1  21975  mplbas2  21980  mplascl  22008  mplmon2cl  22012  mplmon2mul  22013  evlrhm  22042  mpfconst  22047  mhpvscacl  22078  psdascl  22092  vr1cl2  22112  ply1lss  22115  ply1subrg  22116  psropprmul  22156  ply1chr  22225  evl1vsd  22263  evl1expd  22264  evl1gsumadd  22277  evl1gsummon  22284  evls1fpws  22288  evls1vsca  22292  asclply1subcl  22293  evls1maplmhm  22296  matring  22358  matassa  22359  mat1  22362  mattposcl  22368  mavmulass  22464  mdetunilem9  22535  matinv  22592  cpmadugsumlemF  22791  cpmadugsumfi  22792  cpmidgsum2  22794  elcls3  23000  mreclatdemoBAD  23013  neiptopnei  23049  resstps  23104  ordtrest2lem  23120  ordtrest2  23121  pnfnei  23137  mnfnei  23138  iscnp2  23156  iscnp4  23180  cnrest2r  23204  lmcls  23219  lmcld  23220  cnt0  23263  cnhaus  23271  isreg2  23294  connclo  23332  1stccnp  23379  loclly  23404  lly1stc  23413  locfincmp  23443  unisngl  23444  comppfsc  23449  kgencmp2  23463  llycmpkgen2  23467  kgen2ss  23472  kgencn3  23475  pttoponconst  23514  txcls  23521  txbasval  23523  dfac14lem  23534  ptcn  23544  ptrescn  23556  txtube  23557  txcmplem1  23558  txlm  23565  txkgen  23569  xkopjcn  23573  cnmptkp  23597  xkoinjcn  23604  qtopkgen  23627  imastps  23638  isr0  23654  r0cld  23655  pt1hmeo  23723  ptuncnv  23724  ptunhmeo  23725  filintn0  23778  trnei  23809  flimfil  23886  flimopn  23892  fbflim2  23894  cnpflf2  23917  flfcnp  23921  flfcnp2  23924  fclsopn  23931  fcfnei  23952  cnpfcf  23958  flfcntr  23960  alexsublem  23961  ptcmplem3  23971  ptcmplem4  23972  cnextfres1  23985  tmdcn2  24006  tmdgsum  24012  tmdgsum2  24013  efmndtmd  24018  symgtgp  24023  tgphaus  24034  tgpt1  24035  qustgplem  24038  prdstmdd  24041  prdstgpd  24042  haustsms  24053  tsmscls  24055  tsmsmhm  24063  tsmsadd  24064  tgptsmscls  24067  tsmssplit  24069  restutop  24155  utopreg  24170  ressusp  24182  ucncn  24203  xmetunirn  24256  ressprdsds  24290  xpsdsval  24300  xblss2ps  24320  blbas  24349  mopntopon  24358  isxms2  24367  imasf1oxms  24411  imasf1oms  24412  prdsxmslem2  24451  tmsxpsval  24460  tngngp2  24582  tngngp  24584  tgioo  24725  metdseq0  24783  cncfmpt2f  24848  cncfcnvcn  24859  cnmptre  24861  cnheibor  24894  nmhmcn  25060  cvsdiv  25072  cvsdivcl  25073  cphsubrglem  25118  cphreccllem  25119  iscmet3  25234  relcmpcmet  25259  bcthlem4  25268  rrxds  25334  rrxvsca  25335  rrxplusgvscavalb  25336  rrxbasefi  25351  rrxmetfi  25353  minveclem4  25373  mulcncf  25387  ivthicc  25400  evthicc  25401  ovolicc2lem4  25462  ovolicc2lem5  25463  iunmbl2  25499  vitalilem3  25552  cncombf  25600  cnmbf  25601  dvres2lem  25852  cpncn  25879  cpnres  25880  dvaddbr  25881  dvmulbr  25882  dvmulbrOLD  25883  dvcobr  25890  dvcobrOLD  25891  dvcjbr  25894  dvrec  25900  dvcnvlem  25921  dvlip2  25941  dvivth  25956  lhop2  25961  lhop  25962  dvcnvrelem1  25963  dvcnvrelem2  25964  dvcnvre  25965  ftc1lem6  25989  mdegvscale  26024  mdegvsca  26025  fta1blem  26118  plyaddlem1  26160  plymullem1  26161  coeeulem  26171  tayl0  26309  taylthlem1  26321  taylthlem2  26322  taylthlem2OLD  26323  ulmdvlem3  26351  psercnlem2  26374  psercn  26376  efsubm  26498  cxpcn3  26696  loglesqrt  26706  efrlim  26914  efrlimOLD  26915  ppinprm  27097  chtnprm  27099  dchrptlem1  27210  dchrptlem2  27211  nodenselem5  27634  oldlim  27826  cofcutr  27857  addsproplem6  27904  negsproplem6  27958  mulsproplem13  28041  mulsproplem14  28042  noseqp1  28177  tgbtwnouttr2  28312  tgldim0eq  28320  tgifscgr  28325  iscgrglt  28331  ercgrg  28334  tgcgrxfr  28335  motcgrg  28361  tglngne  28367  tgcolg  28371  tgbtwnconn1lem2  28390  tgbtwnconn1lem3  28391  legtri3  28407  legbtwn  28411  ncolne1  28442  tgisline  28444  tglinethru  28453  coltr3  28465  colline  28466  tglowdim2ln  28468  mirinv  28483  miriso  28487  mirauto  28501  miduniq  28502  krippenlem  28507  midexlem  28509  ragperp  28534  footexALT  28535  footexlem2  28537  perpdragALT  28544  perpdrag  28545  colperpexlem1  28547  colperpexlem3  28549  mideulem2  28551  midex  28554  opphllem1  28564  opphllem3  28566  opphllem4  28567  hlpasch  28573  trgcopy  28621  f1otrg  28688  axlowdimlem16  28781  elntg  28808  eengtrkg  28810  eengtrkge  28811  clwwlkccatlem  29812  grpoidinv2  30338  grpoinv  30348  ubthlem2  30694  shuni  31123  acunirnmpt  32458  acunirnmpt2  32459  acunirnmpt2f  32460  fpwrelmap  32528  fzm1ne1  32570  fzom1ne1  32582  ccatf1  32685  swrdf1  32690  gsummpt2d  32776  gsumhashmul  32783  odpmco  32822  pmtrcnel  32825  pmtrcnel2  32826  pmtrcnelor  32827  tocyc01  32852  trsp2cyc  32857  cycpmco2f1  32858  cycpmco2rn  32859  cycpmco2lem1  32860  cycpmco2lem2  32861  cycpmco2lem3  32862  cycpmco2lem4  32863  cycpmco2lem5  32864  cycpmco2lem6  32865  cycpmco2lem7  32866  cycpmco2  32867  cycpmconjv  32876  cycpmrn  32877  tocyccntz  32878  isdrng4  32975  sdrgdvcl  32977  sdrginvcl  32978  rloccring  32997  rloc0g  32998  rloc1r  32999  fracfld  33007  pidlnz  33100  qusmul  33127  nsgmgc  33135  ghmqusnsglem1  33142  rhmquskerlem  33153  rhmqusnsg  33156  elrspunidl  33157  elrspunsn  33158  drngidl  33162  qsidomlem1  33181  mxidlirred  33198  opprmxidlabs  33211  opprqusplusg  33213  opprqusmulr  33215  opprqusdrng  33217  qsdrngilem  33218  qsdrngi  33219  qsdrnglem2  33220  qsdrng  33221  qsfld  33222  idlsrg0g  33230  ressdeg1  33251  ressply1invg  33254  ressply1sub  33255  ply1degltlss  33267  gsummoncoe1fzo  33268  ig1pmindeg  33272  q1pvsca  33274  r1pvsca  33275  srasubrg  33284  drgextlsp  33293  matdim  33313  lbslsat  33314  ply1degltdimlem  33320  ply1degltdim  33321  lindsunlem  33322  lbsdiflsp0  33324  dimkerim  33325  fedgmullem1  33327  fedgmullem2  33328  fedgmul  33329  fldexttr  33350  extdgmul  33353  extdg1id  33355  irngss  33365  irngnzply1lem  33368  irngnzply1  33369  irngnminplynz  33382  algextdeglem4  33388  algextdeglem8  33392  rspectopn  33468  zarclsiin  33472  zarmxt1  33481  rspectps  33484  rhmpreimacn  33486  ordtrest2NEWlem  33523  ordtrest2NEW  33524  lmxrge0  33553  nmmulg  33569  rrhcn  33598  esumadd  33676  esumaddf  33680  esumcocn  33699  measiuns  33836  mbfmco2  33885  dya2iocnrect  33901  omscl  33915  omsf  33916  oms0  33917  sibf0  33954  sibfof  33960  sitgaddlemb  33968  fibp1  34021  ccatmulgnn0dir  34174  cxpcncf1  34227  ftc2re  34230  fsum2dsub  34239  reprf  34244  reprsum  34245  bnj1450  34681  bnj1501  34698  revpfxsfxrev  34725  indispconn  34844  connpconn  34845  pconnpi1  34847  sconnpi1  34849  cvmsss2  34884  cvmliftmolem1  34891  cvmliftlem8  34902  cvmliftlem10  34904  cvmliftlem11  34905  cvmlift2lem9  34921  cvmlift2lem12  34924  cvmlift3lem7  34935  mrsubcv  35120  mrsubff  35122  mrsubccat  35128  elmrsubrn  35130  mrsubco  35131  mrsubvrs  35132  linethru  35749  ivthALT  35819  neibastop2  35845  filnetlem4  35865  matunitlindflem2  37090  poimirlem1  37094  poimirlem2  37095  poimirlem8  37101  poimirlem9  37102  poimirlem16  37109  poimirlem17  37110  poimirlem19  37112  poimirlem20  37113  poimirlem22  37115  poimirlem23  37116  poimir  37126  broucube  37127  areacirclem4  37184  fdc  37218  isbnd3  37257  prdsbnd  37266  prdstotbnd  37267  prdsbnd2  37268  rrnequiv  37308  reheibor  37312  iscringd  37471  isfldidl  37541  eqvrelth  38083  eqlkr  38571  ldualvsubval  38629  dvalveclem  40498  dia2dimlem5  40541  dia2dimlem9  40545  tendoinvcl  40577  dvhgrp  40580  dvhlveclem  40581  dihpN  40809  dochsnkr2cl  40947  lcfl7lem  40972  lclkr  41006  lclkrs  41012  lcfrvalsnN  41014  lcfrlem4  41018  lcfrlem6  41020  lcfrlem16  41031  lcdvsubval  41091  lcdlkreqN  41095  mapdcl2  41129  mapdincl  41134  mapdlsmcl  41136  mapdpglem3  41148  hdmaprnlem9N  41330  hdmaplkr  41386  hdmapip0  41388  hdmapglem7a  41400  ressmulgnnd  41569  remexz  41575  primrootspoweq0  41577  aks6d1c1p3  41581  aks6d1c1p5  41583  aks6d1c2lem4  41598  idomnnzpownz  41603  idomnnzgmulnz  41604  ringexp0nn  41605  aks6d1c5lem0  41606  aks6d1c5lem3  41608  aks6d1c5lem2  41609  aks6d1c5  41610  sticksstones11  41628  sticksstones12a  41629  sticksstones19  41637  aks6d1c6lem2  41643  aks6d1c6lem4  41645  aks6d1c6isolem1  41646  aks6d1c6isolem2  41647  aks6d1c6lem5  41649  evlsscaval  41797  selvvvval  41818  evlselv  41820  mhphf2  41831  mhphf4  41833  prjspnvs  42044  prjspnn0  42046  prjspner1  42050  fltnltalem  42086  diophin  42192  acongeq  42404  isnumbasgrplem2  42528  proot1mul  42622  oacl2g  42759  omabs2  42761  omcl2  42762  iunrelexpuztr  43149  ntrclsiex  43483  ntrneiiex  43506  ntrneinex  43507  elnelneqd  43632  grurankcld  43670  bccbc  43782  suctrALT  44265  restuni3  44484  disjf1o  44564  disjinfi  44565  choicefi  44573  fsneq  44579  fsneqrn  44584  unirnmapsn  44587  iunmapsn  44590  monoords  44679  elfzolem1  44703  uzfissfz  44708  monoord2xrv  44866  evthiccabs  44881  iooabslt  44884  tgqioo2  44932  islptre  45007  limciccioolb  45009  sumnnodd  45018  limcicciooub  45025  lptre2pt  45028  limcresiooub  45030  limcresioolb  45031  lptioo1cn  45034  reclimc  45041  liminfvalxr  45171  liminfvaluz  45180  limsupvaluz3  45186  fsumcncf  45266  ioccncflimc  45273  cncfuni  45274  icccncfext  45275  cncficcgt0  45276  icocncflimc  45277  cncfdmsn  45278  cncfiooicclem1  45281  cncfiooicc  45282  cncfioobd  45285  cxpcncf2  45287  fprodsub2cncf  45293  fprodadd2cncf  45294  fperdvper  45307  dvcosax  45314  dvnmul  45331  dvnprodlem1  45334  dvnprodlem2  45335  itgsubsticclem  45363  fvvolioof  45377  fvvolicof  45379  stoweidlem26  45414  stoweidlem27  45415  stoweidlem31  45419  stoweidlem34  45422  dirkercncflem2  45492  dirkercncflem3  45493  dirkercncflem4  45494  dirkercncf  45495  fourierdlem16  45511  fourierdlem20  45515  fourierdlem21  45516  fourierdlem22  45517  fourierdlem26  45521  fourierdlem32  45527  fourierdlem33  45528  fourierdlem38  45533  fourierdlem39  45534  fourierdlem46  45540  fourierdlem48  45542  fourierdlem49  45543  fourierdlem53  45547  fourierdlem60  45554  fourierdlem61  45555  fourierdlem69  45563  fourierdlem70  45564  fourierdlem71  45565  fourierdlem73  45567  fourierdlem74  45568  fourierdlem75  45569  fourierdlem76  45570  fourierdlem80  45574  fourierdlem81  45575  fourierdlem82  45576  fourierdlem83  45577  fourierdlem84  45578  fourierdlem85  45579  fourierdlem88  45582  fourierdlem89  45583  fourierdlem91  45585  fourierdlem92  45586  fourierdlem93  45587  fourierdlem100  45594  fourierdlem101  45595  fourierdlem103  45597  fourierdlem104  45598  fourierdlem107  45601  fourierdlem111  45605  fourierdlem112  45606  fourierdlem113  45607  fouriersw  45619  fouriercn  45620  etransclem24  45646  etransclem26  45648  etransclem28  45650  etransclem31  45653  etransclem32  45654  etransclem33  45655  etransclem34  45656  etransclem35  45657  etransclem38  45660  rrxtopnfi  45675  rrxtoponfi  45679  qndenserrnbl  45683  qndenserrnopnlem  45685  qndenserrn  45687  rrnprjdstle  45689  ioorrnopnlem  45692  prsal  45706  intsaluni  45717  salgencntex  45731  subsaliuncllem  45745  fge0iccico  45758  sge0sn  45767  sge0tsms  45768  sge0cl  45769  sge0f1o  45770  sge0pr  45782  sge0isum  45815  nnfoctbdjlem  45843  iundjiunlem  45847  iundjiun  45848  meadjiunlem  45853  psmeasure  45859  meaiininclem  45874  caragenelss  45889  omeunile  45893  carageniuncllem1  45909  carageniuncllem2  45910  0ome  45917  isomenndlem  45918  isomennd  45919  hoicvr  45936  ovnpnfelsup  45947  ovncvrrp  45952  ovnsubaddlem1  45958  hoidmv1le  45982  hoidmvlelem2  45984  hoidmvlelem3  45985  hoidmvlelem4  45986  hoidmvle  45988  ovnhoilem1  45989  hoi2toco  45995  ovncvr2  45999  hspdifhsp  46004  voncmpl  46009  hoiqssbl  46013  hspmbllem2  46015  hspmbl  46017  hoimbllem  46018  opnvonmbllem2  46021  mblvon  46027  ovolval3  46035  ovolval4lem1  46037  ovnovollem1  46044  ovnovollem2  46045  vonsn  46079  issmflem  46115  sssmf  46126  issmflelem  46132  issmfgtlem  46143  issmfgt  46144  smfaddlem1  46151  issmfgelem  46157  smflimlem3  46161  smfmullem2  46180  smfmullem4  46182  smfsuplem1  46199  smfsupmpt  46203  smfinfmpt  46207  smflimsuplem2  46209  smflimsuplem4  46211  smflimsupmpt  46217  smfliminfmpt  46220  fsupdm  46230  finfdm  46234  fzoopth  46707  zlmodzxzel  47419  ply1mulgsum  47458  catprs  48017  thincmod  48037  mndtcob  48094  mndtccatid  48099  mndtcid  48101  grptcmon  48102  grptcepi  48103

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »