Theorem eleqtrrdi 2836

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 2734	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2835	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802

This theorem is referenced by:  3eltr4g  2842  brelrng  5943  elabrex  7252  elabrexg  7253  fliftel1  7317  ovidig  7563  unielxp  8032  tfrlem11  8409  rdglim  8447  seqomlem4  8474  2oconcl  8524  ecopqsi  8793  erov  8833  eroprf  8834  sbthlem2  9109  dffi3  9456  ixpiunwdom  9615  cantnfcl  9692  r1lim  9797  rankwflemb  9818  pwwf  9832  unwf  9835  rankwflem  9840  uniwf  9844  rankpwi  9848  rankr1g  9857  r1pw  9870  r1rankid  9884  rankuni  9888  djulcl  9935  djurcl  9936  inlresf  9939  inrresf  9941  djuun  9951  cardlim  9997  infxpenlem  10038  alephfp  10133  cfsmolem  10295  alephsing  10301  hsmexlem4  10454  axdc3lem2  10476  numth3  10495  iunfo  10564  konigthlem  10593  iunctb  10599  canthwelem  10675  canthwe  10676  r1limwun  10761  inar1  10800  inatsk  10803  gruina  10843  grur1  10845  tskmval  10864  tskmcl  10866  pinq  10952  dmrecnq  10993  addclsr  11108  mulclsr  11109  axaddf  11170  axmulf  11171  peano2nn  12257  uztrn2  12874  eluz2nn  12901  peano2uzs  12919  uzsupss  12957  uzsup  13864  uzrdgfni  13959  uzrdgsuci  13961  fsuppmapnn0fiub  13992  seqf  14024  ser0  14055  bcm1k  14310  bcp1nk  14312  bcpasc  14316  hashprdifel  14393  fz1isolem  14458  pr2pwpr  14476  ccats1val2  14613  rexuzre  15335  limsupgre  15461  climconst  15523  rlimclim1  15525  climrlim2  15527  clim2ser  15637  clim2ser2  15638  iserex  15639  isermulc2  15640  iserle  15642  isercolllem3  15649  isercoll2  15651  climsup  15652  iseraltlem2  15665  iseraltlem3  15666  zsum  15700  isumclim3  15741  isumadd  15749  fsump1i  15751  iserabs  15797  cvgcmp  15798  cvgcmpub  15799  cvgcmpce  15800  abscvgcvg  15801  isumshft  15821  isumsplit  15822  isum1p  15823  isumrpcl  15825  isumsup2  15828  climcndslem1  15831  cvgrat  15865  clim2prod  15870  clim2div  15871  prodf1  15873  ntrivcvgn0  15880  ntrivcvgtail  15882  fprodntriv  15922  fprodabs  15954  fprodeq0  15955  iprodclim3  15980  iprodmul  15983  ef0lem  16058  fprodefsum  16075  rpnnen2lem3  16196  dvdsflip  16297  fzo0dvdseq  16303  bitsinv1  16420  smupval  16466  smueqlem  16468  seq1st  16545  algr0  16546  prmind2  16659  crth  16750  eulerthlem2  16754  prmdiv  16757  pockthlem  16877  pockthg  16878  unbenlem  16880  prmunb  16886  prmgaplem7  17029  strfv2d  17174  imasvscaval  17523  oppccatid  17704  oppccatf  17713  epii  17729  fthepi  17920  funcestrcsetclem3  18136  funcsetcestrclem3  18150  yon12  18260  yon2  18261  yonedalem4c  18272  yonedalem22  18273  yonedalem3b  18274  yonedainv  18276  acsmapd  18549  mgm2nsgrplem1  18878  mgm2nsgrplem2  18879  mgm2nsgrplem3  18880  sgrp2nmndlem1  18883  sgrp2rid2  18886  ghmqusker  19250  cntrsubgnsg  19306  symgpssefmnd  19362  pmtrrn  19424  gexcl3  19554  efgi  19686  efgi2  19692  efgs1b  19703  efgredlemg  19709  efgredlemd  19711  frgpnabllem1  19840  cycsubgcyg  19868  gsumzaddlem  19888  dprdwd  19980  dprd2da  20011  rhmopp  20460  lsppratlem3  21049  lsppratlem4  21050  lbsextlem2  21059  lidl0ALT  21136  lidl1ALT  21139  2idl0  21167  2idl1  21168  domnchr  21479  znf1o  21502  mplsubrglem  21966  mpfconst  22069  mpfproj  22070  mpfind  22075  mhpmulcl  22096  pf1const  22290  pf1id  22291  mpfpf1  22295  pf1mpf  22296  madetsumid  22407  slesolex  22628  pmatcoe1fsupp  22647  mat2pmatbas0  22673  pmatcollpw  22727  pm2mpf1  22745  isclo  23035  indiscld  23039  restntr  23130  ordtbaslem  23136  ordtbas2  23139  lmconst  23209  lmss  23246  conncompid  23379  2ndcomap  23406  locfincmp  23474  comppfsc  23480  xkouni  23547  txcls  23552  ptclsg  23563  uptx  23573  txindis  23582  tx1stc  23598  cnmpt1res  23624  tgqtop  23660  uffix  23869  cnpflf2  23948  ptcmplem2  24001  ptcmplem4  24003  tgpconncomp  24061  tsmsfbas  24076  fmucnd  24241  prdsxmetlem  24318  imasdsf1olem  24323  prdsbl  24444  blcvx  24758  xrsmopn  24772  xrge0tsms  24794  metdcn2  24799  expcncf  24891  cnmpopc  24893  icchmeo  24909  icchmeoOLD  24910  iccpnfhmeo  24914  cnheibor  24925  evth  24929  evth2  24930  lebnumlem2  24932  lebnumii  24936  reparphti  24967  reparphtiOLD  24968  cfilfcls  25246  minveclem2  25398  minveclem3  25401  minveclem4  25404  ovoliunlem1  25475  ovolicc1  25489  iundisj  25521  volsup  25529  uniioombllem3  25558  vitalilem2  25582  vitalilem3  25583  mbfsup  25637  mbfinf  25638  mbflimsup  25639  itg2monolem1  25724  limcflflem  25853  limccnp  25864  limccnp2  25865  dvidlem  25888  dvn2bss  25904  cpnres  25911  dvcobr  25921  dvcobrOLD  25922  dvrec  25931  c1liplem1  25973  dvcnvrelem2  25995  dvfsumrlimf  26003  dvfsumlem1  26004  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem3  26007  dvfsumlem4  26008  dvfsumrlim  26010  dvfsum2  26013  coeeulem  26203  coeid3  26219  plycn  26240  plycnOLD  26241  dvntaylp  26351  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulm2  26366  ulmshftlem  26370  ulmshft  26371  ulm0  26372  ulmcn  26380  ulmdvlem3  26383  ulmdv  26384  mtest  26385  mtestbdd  26386  dvradcnv  26402  psercn2  26404  psercn2OLD  26405  psercn  26408  pserdv  26411  abelth  26423  efif1olem2  26522  efif1olem4  26524  efifo  26526  eff1olem  26527  logcn  26626  dvloglem  26627  cxpcn3  26728  resqrtcn  26729  sqrtcn  26730  logbleb  26760  logblt  26761  asinneg  26863  atanlogsub  26893  atanbnd  26903  ressatans  26911  leibpilem2  26918  xrlimcnp  26945  efrlim  26946  efrlimOLD  26947  scvxcvx  26963  ppiub  27182  chtub  27190  logexprlim  27203  lgseisenlem1  27353  rplogsumlem1  27462  rplogsumlem2  27463  dchrisumlem2  27468  dchrisum0flb  27488  logdivbnd  27534  pntlem3  27587  tgcgr4  28407  ltgov  28473  f1otrg  28747  eengtrkg  28869  iedgedg  28935  ushgredgedgloop  29116  subgruhgredgd  29169  uvtxupgrres  29293  umgr2v2evd2  29413  edginwlk  29521  wlk1walk  29525  crctcshwlkn0lem6  29698  wlkiswwlks1  29750  minvecolem1  30756  minvecolem2  30757  minvecolem4  30762  htthlem  30799  5oalem2  31537  3oalem2  31545  iundisjf  32458  fmptco1f1o  32499  xppreima  32513  xppreima2  32518  dfcnv2  32543  ccatws1f1o  32761  gsumhashmul  32860  xrge0tsmsd  32861  odpmco  32899  pmtrcnelor  32904  fzo0pmtrlast  32905  wrdpmtrlast  32906  pmtrto1cl  32912  psgnfzto1stlem  32913  fzto1stfv1  32914  fzto1st  32916  fzto1stinvn  32917  psgnfzto1st  32918  tocycf  32930  cycpmco2lem7  32945  cycpmco2  32946  cycpmrn  32956  cyc3evpm  32963  cyc3genpmlem  32964  cycpmgcl  32966  cyc3conja  32970  nsgmgc  33224  nsgqusf1olem1  33225  nsgqusf1olem2  33226  rhmpreimaprmidl  33263  ssdifidllem  33268  ssdifidl  33269  ssmxidllem  33285  drngmxidlr  33290  opprqus1r  33304  qsdrngilem  33306  qsdrngi  33307  rsprprmprmidlb  33335  rprmirredb  33344  1arithufdlem1  33359  1arithufdlem2  33360  1arithufdlem3  33361  1arithufdlem4  33362  fply1  33371  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  ply1degltdimlem  33451  ply1degltdim  33452  algextdeglem4  33519  algextdeglem6  33521  algextdeglem7  33522  algextdeglem8  33523  smatlem  33529  smatcl  33534  zartopn  33607  zarmxt1  33612  tpr2rico  33644  xrmulc1cn  33662  xrge0mulc1cn  33673  esumpfinvallem  33824  ldgenpisyslem1  33913  dynkin  33917  brfae  33998  sxbrsigalem3  34023  dya2icoseg2  34029  omsmeas  34074  sibfof  34091  sseqmw  34142  sseqf  34143  sseqp1  34146  fiblem  34149  fibp1  34152  probfinmeasbALTV  34180  repr0  34374  reprpmtf1o  34389  hgt750lemg  34417  bnj1379  34592  srcmpltd  34836  subfacp1lem5  34925  subfacp1lem6  34926  cvxpconn  34983  cvxsconn  34984  cvmliftlem6  35031  cvmliftlem8  35033  cvmliftlem10  35035  cvmlift2lem6  35049  cvmlift2lem11  35054  cvmlift2lem12  35055  2goelgoanfmla1  35165  prv1n  35172  msubff  35271  msubco  35272  elmsta  35289  msubff1  35297  mvhf  35299  msubvrs  35301  iprodefisumlem  35465  filnetlem3  35995  knoppcnlem10  36108  knoppcnlem11  36109  icoreunrn  36969  icoreelrn  36971  ralssiun  37017  poimirlem3  37227  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem30  37254  dvasin  37308  cover2  37319  upixp  37333  sdclem1  37347  fdc  37349  caushft  37365  ismtyres  37412  rrncmslem  37436  isfld2  37609  osumcllem10N  39568  pexmidlem7N  39579  dihglblem2N  40897  lcfrvalsnN  41144  lcfrlem5  41149  lcfrlem6  41150  lcfrlem27  41172  lcfrlem37  41182  aks6d1c1p4  41714  aks6d1c1p7  41716  aks6d1c1p8  41718  evl1gprodd  41720  aks6d1c2lem4  41730  aks6d1c5lem3  41740  aks6d1c6lem2  41774  prjspvs  42169  0prjspnrel  42186  monotuz  42504  expdiophlem1  42584  kelac2  42631  naddwordnexlem4  42973  grurankcld  43812  dvgrat  43891  nzss  43896  uzmptshftfval  43925  binomcxplemnotnn0  43935  refsumcn  44534  rfcnpre2  44535  rfcnpre3  44537  rfcnpre4  44538  disjf1o  44703  unirnmap  44720  unirnmapsn  44726  ssmapsn  44728  mptssid  44754  allbutfi  44913  eluzd  44929  uzidd2  44936  ressiocsup  45077  ressioosup  45078  ressiooinf  45080  fsumsermpt  45105  climexp  45131  climinf  45132  climsuse  45134  sumnnodd  45156  limsupresico  45226  limsupubuzlem  45238  limsupresxr  45292  liminfresxr  45293  liminfresico  45297  limsup10exlem  45298  cnrefiisplem  45355  cncfiooicclem1  45419  dvsinax  45439  itgsinexplem1  45480  fvvolioof  45515  fvvolicof  45517  stoweidlem14  45540  stoweidlem16  45542  stoweidlem31  45557  stoweidlem34  45560  stoweidlem36  45562  stoweidlem43  45569  stoweidlem46  45572  stoweidlem47  45573  stoweidlem52  45578  stoweidlem55  45581  stoweidlem57  45583  dirkercncf  45633  fourierdlem20  45653  fourierdlem42  45675  fourierdlem48  45680  fourierdlem49  45681  fourierdlem51  45683  fourierdlem54  45686  fourierdlem62  45694  fourierdlem71  45703  fourierdlem80  45712  fourierdlem114  45746  fouriersw  45757  ioorrnopnlem  45830  ioorrnopnxrlem  45832  salexct3  45868  salgencntex  45869  salgensscntex  45870  subsalsal  45885  sge0fodjrnlem  45942  sge0isum  45953  sge0seq  45972  sge0reuz  45973  sge0reuzb  45974  meadjiunlem  45991  meaiininclem  46012  carageniuncllem1  46047  caratheodorylem1  46052  hoiprodp1  46114  hoidmv1lelem1  46117  hoidmv1lelem2  46118  hoidmv1le  46120  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem3  46123  voncmpl  46147  hoiqssbl  46151  smflimlem2  46298  smfsuplem1  46337  smfsuplem3  46339  fsupdm  46368  finfdm  46372  cfsetsnfsetf  46578  fcores  46587  afvres  46690  afv2res  46757  fundcmpsurinjimaid  46888  iccpartigtl  46900  sprsymrelf  46972  prproropf1olem2  46981  isuspgrim0lem  47355  isuspgrimlem  47358  ushggricedg  47379  funcringcsetcALTV2lem3  47540  funcringcsetclem3ALTV  47563  lindslinindsimp2lem5  47716  rrxsphere  48007  line2  48011  iooii  48122  icccldii  48123  iscnrm3rlem3  48147  onsetreclem3  48324  amgmwlem  48421