Theorem eleqtrrdi 2839

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2738	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2838	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  3eltr4g  2845  brelrng  5905  elabrex  7216  elabrexg  7217  fliftel1  7285  ovidig  7531  unielxp  8006  tfrlem11  8356  rdglim  8394  seqomlem4  8421  2oconcl  8467  ecopqsi  8744  erov  8787  eroprf  8788  sbthlem2  9052  dffi3  9382  ixpiunwdom  9543  cantnfcl  9620  r1lim  9725  rankwflemb  9746  pwwf  9760  unwf  9763  rankwflem  9768  uniwf  9772  rankpwi  9776  rankr1g  9785  r1pw  9798  r1rankid  9812  rankuni  9816  djulcl  9863  djurcl  9864  inlresf  9867  inrresf  9869  djuun  9879  cardlim  9925  infxpenlem  9966  alephfp  10061  cfsmolem  10223  alephsing  10229  hsmexlem4  10382  axdc3lem2  10404  numth3  10423  iunfo  10492  konigthlem  10521  iunctb  10527  canthwelem  10603  canthwe  10604  r1limwun  10689  inar1  10728  inatsk  10731  gruina  10771  grur1  10773  tskmval  10792  tskmcl  10794  pinq  10880  dmrecnq  10921  addclsr  11036  mulclsr  11037  axaddf  11098  axmulf  11099  peano2nn  12198  uztrn2  12812  eluz2nn  12847  peano2uzs  12861  uzsupss  12899  uzsup  13825  uzrdgfni  13923  uzrdgsuci  13925  fsuppmapnn0fiub  13956  seqf  13988  ser0  14019  bcm1k  14280  bcp1nk  14282  bcpasc  14286  hashprdifel  14363  fz1isolem  14426  pr2pwpr  14444  tpf  14464  ccats1val2  14592  rexuzre  15319  limsupgre  15447  climconst  15509  rlimclim1  15511  climrlim2  15513  clim2ser  15621  clim2ser2  15622  iserex  15623  isermulc2  15624  iserle  15626  isercolllem3  15633  isercoll2  15635  climsup  15636  iseraltlem2  15649  iseraltlem3  15650  zsum  15684  isumclim3  15725  isumadd  15733  fsump1i  15735  iserabs  15781  cvgcmp  15782  cvgcmpub  15783  cvgcmpce  15784  abscvgcvg  15785  isumshft  15805  isumsplit  15806  isum1p  15807  isumrpcl  15809  isumsup2  15812  climcndslem1  15815  cvgrat  15849  clim2prod  15854  clim2div  15855  prodf1  15857  ntrivcvgn0  15864  ntrivcvgtail  15866  fprodntriv  15908  fprodabs  15940  fprodeq0  15941  iprodclim3  15966  iprodmul  15969  ef0lem  16044  fprodefsum  16061  rpnnen2lem3  16184  dvdsflip  16287  fzo0dvdseq  16293  bitsinv1  16412  smupval  16458  smueqlem  16460  seq1st  16541  algr0  16542  prmind2  16655  crth  16748  eulerthlem2  16752  prmdiv  16755  pockthlem  16876  pockthg  16877  unbenlem  16879  prmunb  16885  prmgaplem7  17028  strfv2d  17171  imasvscaval  17501  oppccatid  17680  oppccatf  17689  epii  17705  fthepi  17892  funcestrcsetclem3  18103  funcsetcestrclem3  18117  yon12  18226  yon2  18227  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedainv  18242  acsmapd  18513  mgm2nsgrplem1  18845  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem1  18850  sgrp2rid2  18853  ghmqusker  19219  cntrsubgnsg  19275  symgpssefmnd  19326  pmtrrn  19387  gexcl3  19517  efgi  19649  efgi2  19655  efgs1b  19666  efgredlemg  19672  efgredlemd  19674  frgpnabllem1  19803  cycsubgcyg  19831  gsumzaddlem  19851  dprdwd  19943  dprd2da  19974  rhmopp  20418  lsppratlem3  21059  lsppratlem4  21060  lbsextlem2  21069  lidl0ALT  21138  lidl1ALT  21141  2idl0  21170  2idl1  21171  domnchr  21442  znf1o  21461  mplsubrglem  21913  mpfconst  22008  mpfproj  22009  mpfind  22014  mhpmulcl  22036  pf1const  22233  pf1id  22234  mpfpf1  22238  pf1mpf  22239  madetsumid  22348  slesolex  22569  pmatcoe1fsupp  22588  mat2pmatbas0  22614  pmatcollpw  22668  pm2mpf1  22686  isclo  22974  indiscld  22978  restntr  23069  ordtbaslem  23075  ordtbas2  23078  lmconst  23148  lmss  23185  conncompid  23318  2ndcomap  23345  locfincmp  23413  comppfsc  23419  xkouni  23486  txcls  23491  ptclsg  23502  uptx  23512  txindis  23521  tx1stc  23537  cnmpt1res  23563  tgqtop  23599  uffix  23808  cnpflf2  23887  ptcmplem2  23940  ptcmplem4  23942  tgpconncomp  24000  tsmsfbas  24015  fmucnd  24179  prdsxmetlem  24256  imasdsf1olem  24261  prdsbl  24379  blcvx  24686  xrsmopn  24701  xrge0tsms  24723  metdcn2  24728  expcncf  24820  cnmpopc  24822  icchmeo  24838  icchmeoOLD  24839  iccpnfhmeo  24843  cnheibor  24854  evth  24858  evth2  24859  lebnumlem2  24861  lebnumii  24865  reparphti  24896  reparphtiOLD  24897  cfilfcls  25174  minveclem2  25326  minveclem3  25329  minveclem4  25332  ovoliunlem1  25403  ovolicc1  25417  iundisj  25449  volsup  25457  uniioombllem3  25486  vitalilem2  25510  vitalilem3  25511  mbfsup  25565  mbfinf  25566  mbflimsup  25567  itg2monolem1  25651  limcflflem  25781  limccnp  25792  limccnp2  25793  dvidlem  25816  dvn2bss  25832  cpnres  25839  dvcobr  25849  dvcobrOLD  25850  dvrec  25859  c1liplem1  25901  dvcnvrelem2  25923  dvfsumrlimf  25931  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlim  25938  dvfsum2  25941  coeeulem  26129  coeid3  26145  plycn  26166  plycnOLD  26167  dvntaylp  26279  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulm2  26294  ulmshftlem  26298  ulmshft  26299  ulm0  26300  ulmcn  26308  ulmdvlem3  26311  ulmdv  26312  mtest  26313  mtestbdd  26314  dvradcnv  26330  psercn2  26332  psercn2OLD  26333  psercn  26336  pserdv  26339  abelth  26351  efif1olem2  26452  efif1olem4  26454  efifo  26456  eff1olem  26457  logcn  26556  dvloglem  26557  cxpcn3  26658  resqrtcn  26659  sqrtcn  26660  logbleb  26693  logblt  26694  asinneg  26796  atanlogsub  26826  atanbnd  26836  ressatans  26844  leibpilem2  26851  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  scvxcvx  26896  ppiub  27115  chtub  27123  logexprlim  27136  lgseisenlem1  27286  rplogsumlem1  27395  rplogsumlem2  27396  dchrisumlem2  27401  dchrisum0flb  27421  logdivbnd  27467  pntlem3  27520  dfnns2  28261  tgcgr4  28458  ltgov  28524  f1otrg  28798  eengtrkg  28913  iedgedg  28977  ushgredgedgloop  29158  subgruhgredgd  29211  uvtxupgrres  29335  umgr2v2evd2  29455  edginwlk  29563  wlk1walk  29567  crctcshwlkn0lem6  29745  wlkiswwlks1  29797  minvecolem1  30803  minvecolem2  30804  minvecolem4  30809  htthlem  30846  5oalem2  31584  3oalem2  31592  iundisjf  32518  fmptco1f1o  32557  xppreima  32569  xppreima2  32575  dfcnv2  32600  ccatws1f1o  32873  chnub  32938  chnccats1  32941  gsumhashmul  33001  xrge0tsmsd  33002  gsumwrd2dccatlem  33006  odpmco  33043  pmtrcnelor  33048  fzo0pmtrlast  33049  wrdpmtrlast  33050  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1stfv1  33058  fzto1st  33060  fzto1stinvn  33061  psgnfzto1st  33062  tocycf  33074  cycpmco2lem7  33089  cycpmco2  33090  cycpmrn  33100  cyc3evpm  33107  cyc3genpmlem  33108  cycpmgcl  33110  cyc3conja  33114  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  nsgmgc  33383  nsgqusf1olem1  33384  nsgqusf1olem2  33385  rhmpreimaprmidl  33422  ssdifidllem  33427  ssdifidl  33428  ssmxidllem  33444  drngmxidlr  33449  opprqus1r  33463  qsdrngilem  33465  qsdrngi  33466  rsprprmprmidlb  33494  rprmirredb  33503  1arithufdlem1  33515  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  fply1  33527  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  ply1degltdimlem  33618  ply1degltdim  33619  algextdeglem4  33710  algextdeglem6  33712  algextdeglem7  33713  algextdeglem8  33714  nn0constr  33751  smatlem  33787  smatcl  33792  zartopn  33865  zarmxt1  33870  tpr2rico  33902  xrmulc1cn  33920  xrge0mulc1cn  33931  esumpfinvallem  34064  ldgenpisyslem1  34153  dynkin  34157  brfae  34238  sxbrsigalem3  34263  dya2icoseg2  34269  omsmeas  34314  sibfof  34331  sseqmw  34382  sseqf  34383  sseqp1  34386  fiblem  34389  fibp1  34392  probfinmeasbALTV  34420  repr0  34602  reprpmtf1o  34617  hgt750lemg  34645  bnj1379  34820  srcmpltd  35070  subfacp1lem5  35171  subfacp1lem6  35172  cvxpconn  35229  cvxsconn  35230  cvmliftlem6  35277  cvmliftlem8  35279  cvmliftlem10  35281  cvmlift2lem6  35295  cvmlift2lem11  35300  cvmlift2lem12  35301  2goelgoanfmla1  35411  prv1n  35418  msubff  35517  msubco  35518  elmsta  35535  msubff1  35543  mvhf  35545  msubvrs  35547  iprodefisumlem  35727  filnetlem3  36368  knoppcnlem10  36490  knoppcnlem11  36491  icoreunrn  37347  icoreelrn  37349  ralssiun  37395  poimirlem3  37617  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem30  37644  dvasin  37698  cover2  37709  upixp  37723  sdclem1  37737  fdc  37739  caushft  37755  ismtyres  37802  rrncmslem  37826  isfld2  37999  osumcllem10N  39959  pexmidlem7N  39970  dihglblem2N  41288  lcfrvalsnN  41535  lcfrlem5  41540  lcfrlem6  41541  lcfrlem27  41563  lcfrlem37  41573  aks6d1c1p4  42099  aks6d1c1p7  42101  aks6d1c1p8  42103  evl1gprodd  42105  aks6d1c2lem4  42115  aks6d1c5lem3  42125  aks6d1c6lem2  42159  prjspvs  42598  0prjspnrel  42615  monotuz  42930  expdiophlem1  43010  kelac2  43054  naddwordnexlem4  43390  grurankcld  44222  dvgrat  44301  nzss  44306  uzmptshftfval  44335  binomcxplemnotnn0  44345  orbitinit  44946  orbitcl  44947  permaxinf2lem  45002  refsumcn  45024  rfcnpre2  45025  rfcnpre3  45027  rfcnpre4  45028  disjf1o  45185  unirnmap  45202  unirnmapsn  45208  ssmapsn  45210  mptssid  45235  allbutfi  45389  eluzd  45405  uzidd2  45412  ressiocsup  45552  ressioosup  45553  ressiooinf  45555  fsumsermpt  45577  climexp  45603  climinf  45604  climsuse  45606  sumnnodd  45628  limsupresico  45698  limsupubuzlem  45710  limsupresxr  45764  liminfresxr  45765  liminfresico  45769  limsup10exlem  45770  cnrefiisplem  45827  cncfiooicclem1  45891  dvsinax  45911  itgsinexplem1  45952  fvvolioof  45987  fvvolicof  45989  stoweidlem14  46012  stoweidlem16  46014  stoweidlem31  46029  stoweidlem34  46032  stoweidlem36  46034  stoweidlem43  46041  stoweidlem46  46044  stoweidlem47  46045  stoweidlem52  46050  stoweidlem55  46053  stoweidlem57  46055  dirkercncf  46105  fourierdlem20  46125  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem62  46166  fourierdlem71  46175  fourierdlem80  46184  fourierdlem114  46218  fouriersw  46229  ioorrnopnlem  46302  ioorrnopnxrlem  46304  salexct3  46340  salgencntex  46341  salgensscntex  46342  subsalsal  46357  sge0fodjrnlem  46414  sge0isum  46425  sge0seq  46444  sge0reuz  46445  sge0reuzb  46446  meadjiunlem  46463  meaiininclem  46484  carageniuncllem1  46519  caratheodorylem1  46524  hoiprodp1  46586  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  voncmpl  46619  hoiqssbl  46623  smflimlem2  46770  smfsuplem1  46809  smfsuplem3  46811  fsupdm  46840  finfdm  46844  cfsetsnfsetf  47059  fcores  47068  afvres  47173  afv2res  47240  fundcmpsurinjimaid  47412  iccpartigtl  47424  sprsymrelf  47496  prproropf1olem2  47505  uhgrimedgi  47890  isuspgrim0lem  47893  isuspgrimlem  47895  ushggricedg  47927  grimedg  47935  usgrgrtrirex  47949  isubgr3stgrlem7  47971  uspgrlimlem4  47990  gpgiedgdmellem  48037  gpg3kgrtriex  48080  funcringcsetcALTV2lem3  48280  funcringcsetclem3ALTV  48303  lindslinindsimp2lem5  48451  rrxsphere  48737  line2  48741  iooii  48906  icccldii  48907  iscnrm3rlem3  48930  eloppf2  49123  oppcup  49196  natoppf  49218  zeroo2  49223  oppfdiag1  49403  oppfdiag  49405  2arwcat  49589  incat  49590  lmddu  49656  onsetreclem3  49696  amgmwlem  49791