Theorem eleqtrrdi 2851

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  3eltr4g  2857  brelrng  5853  elabrex  7125  fliftel1  7190  ovidig  7424  unielxp  7878  tfrlem11  8228  rdglim  8266  seqomlem4  8293  2oconcl  8342  ecopqsi  8572  erov  8612  eroprf  8613  sbthlem2  8880  dffi3  9199  ixpiunwdom  9358  cantnfcl  9434  r1lim  9539  rankwflemb  9560  pwwf  9574  unwf  9577  rankwflem  9582  uniwf  9586  rankpwi  9590  rankr1g  9599  r1pw  9612  r1rankid  9626  rankuni  9630  djulcl  9677  djurcl  9678  inlresf  9681  inrresf  9683  djuun  9693  cardlim  9739  infxpenlem  9778  alephfp  9873  cfsmolem  10035  alephsing  10041  hsmexlem4  10194  axdc3lem2  10216  numth3  10235  iunfo  10304  konigthlem  10333  iunctb  10339  canthwelem  10415  canthwe  10416  r1limwun  10501  inar1  10540  inatsk  10543  gruina  10583  grur1  10585  tskmval  10604  tskmcl  10606  pinq  10692  dmrecnq  10733  addclsr  10848  mulclsr  10849  axaddf  10910  axmulf  10911  peano2nn  11994  uztrn2  12610  eluz2nn  12633  peano2uzs  12651  uzsupss  12689  uzsup  13592  uzrdgfni  13687  uzrdgsuci  13689  fsuppmapnn0fiub  13720  seqf  13753  ser0  13784  bcm1k  14038  bcp1nk  14040  bcpasc  14044  hashprdifel  14122  fz1isolem  14184  pr2pwpr  14202  ccats1val2  14343  rexuzre  15073  limsupgre  15199  climconst  15261  rlimclim1  15263  climrlim2  15265  clim2ser  15375  clim2ser2  15376  iserex  15377  isermulc2  15378  iserle  15380  isercolllem3  15387  isercoll2  15389  climsup  15390  iseraltlem2  15403  iseraltlem3  15404  zsum  15439  isumclim3  15480  isumadd  15488  fsump1i  15490  iserabs  15536  cvgcmp  15537  cvgcmpub  15538  cvgcmpce  15539  abscvgcvg  15540  isumshft  15560  isumsplit  15561  isum1p  15562  isumrpcl  15564  isumsup2  15567  climcndslem1  15570  cvgrat  15604  clim2prod  15609  clim2div  15610  prodf1  15612  ntrivcvgn0  15619  ntrivcvgtail  15621  fprodntriv  15661  fprodabs  15693  fprodeq0  15694  iprodclim3  15719  iprodmul  15722  ef0lem  15797  fprodefsum  15813  rpnnen2lem3  15934  dvdsflip  16035  fzo0dvdseq  16041  bitsinv1  16158  smupval  16204  smueqlem  16206  seq1st  16285  algr0  16286  prmind2  16399  crth  16488  eulerthlem2  16492  prmdiv  16495  pockthlem  16615  pockthg  16616  unbenlem  16618  prmunb  16624  prmgaplem7  16767  strfv2d  16912  imasvscaval  17258  oppccatid  17439  oppccatf  17448  epii  17464  fthepi  17653  funcestrcsetclem3  17868  funcsetcestrclem3  17882  yon12  17992  yon2  17993  yonedalem4c  18004  yonedalem22  18005  yonedalem3b  18006  yonedainv  18008  acsmapd  18281  mgm2nsgrplem1  18566  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  sgrp2nmndlem1  18571  sgrp2rid2  18574  cntrsubgnsg  18956  symgpssefmnd  19012  pmtrrn  19074  gexcl3  19201  efgi  19334  efgi2  19340  efgs1b  19351  efgredlemg  19357  efgredlemd  19359  frgpnabllem1  19483  cycsubgcyg  19511  gsumzaddlem  19531  dprdwd  19623  dprd2da  19654  lsppratlem3  20420  lsppratlem4  20421  lbsextlem2  20430  lidl0  20499  lidl1  20500  domnchr  20745  znf1o  20768  mplsubrglem  21219  mpfconst  21320  mpfproj  21321  mpfind  21326  mhpmulcl  21348  pf1const  21521  pf1id  21522  mpfpf1  21526  pf1mpf  21527  madetsumid  21619  slesolex  21840  pmatcoe1fsupp  21859  mat2pmatbas0  21885  pmatcollpw  21939  pm2mpf1  21957  isclo  22247  indiscld  22251  restntr  22342  ordtbaslem  22348  ordtbas2  22351  lmconst  22421  lmss  22458  conncompid  22591  2ndcomap  22618  locfincmp  22686  comppfsc  22692  xkouni  22759  txcls  22764  ptclsg  22775  uptx  22785  txindis  22794  tx1stc  22810  cnmpt1res  22836  tgqtop  22872  uffix  23081  cnpflf2  23160  ptcmplem2  23213  ptcmplem4  23215  tgpconncomp  23273  tsmsfbas  23288  fmucnd  23453  prdsxmetlem  23530  imasdsf1olem  23535  prdsbl  23656  blcvx  23970  xrsmopn  23984  xrge0tsms  24006  metdcn2  24011  expcncf  24098  cnmpopc  24100  icchmeo  24113  iccpnfhmeo  24117  cnheibor  24127  evth  24131  evth2  24132  lebnumlem2  24134  lebnumii  24138  reparphti  24169  cfilfcls  24447  minveclem2  24599  minveclem3  24602  minveclem4  24605  ovoliunlem1  24675  ovolicc1  24689  iundisj  24721  volsup  24729  uniioombllem3  24758  vitalilem2  24782  vitalilem3  24783  mbfsup  24837  mbfinf  24838  mbflimsup  24839  itg2monolem1  24924  limcflflem  25053  limccnp  25064  limccnp2  25065  dvidlem  25088  dvn2bss  25103  cpnres  25110  dvcobr  25119  dvrec  25128  c1liplem1  25169  dvcnvrelem2  25191  dvfsumrlimf  25198  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlim  25204  dvfsum2  25207  coeeulem  25394  coeid3  25410  plycn  25431  dvntaylp  25539  taylthlem1  25541  taylthlem2  25542  ulm2  25553  ulmshftlem  25557  ulmshft  25558  ulm0  25559  ulmcn  25567  ulmdvlem3  25570  ulmdv  25571  mtest  25572  mtestbdd  25573  dvradcnv  25589  psercn2  25591  psercn  25594  pserdv  25597  abelth  25609  efif1olem2  25708  efif1olem4  25710  efifo  25712  eff1olem  25713  logcn  25811  dvloglem  25812  cxpcn3  25910  resqrtcn  25911  sqrtcn  25912  logbleb  25942  logblt  25943  asinneg  26045  atanlogsub  26075  atanbnd  26085  ressatans  26093  leibpilem2  26100  xrlimcnp  26127  efrlim  26128  scvxcvx  26144  ppiub  26361  chtub  26369  logexprlim  26382  lgseisenlem1  26532  rplogsumlem1  26641  rplogsumlem2  26642  dchrisumlem2  26647  dchrisum0flb  26667  logdivbnd  26713  pntlem3  26766  tgcgr4  26901  ltgov  26967  f1otrg  27241  eengtrkg  27363  iedgedg  27429  ushgredgedgloop  27607  subgruhgredgd  27660  uvtxupgrres  27784  umgr2v2evd2  27903  edginwlk  28011  wlk1walk  28015  crctcshwlkn0lem6  28189  wlkiswwlks1  28241  minvecolem1  29245  minvecolem2  29246  minvecolem4  29251  htthlem  29288  5oalem2  30026  3oalem2  30034  iundisjf  30937  fmptco1f1o  30977  xppreima  30992  xppreima2  30997  dfcnv2  31022  gsumhashmul  31325  xrge0tsmsd  31326  odpmco  31364  pmtrcnelor  31369  pmtrto1cl  31375  psgnfzto1stlem  31376  fzto1stfv1  31377  fzto1st  31379  fzto1stinvn  31380  psgnfzto1st  31381  tocycf  31393  cycpmco2lem7  31408  cycpmco2  31409  cycpmrn  31419  cyc3evpm  31426  cyc3genpmlem  31427  cycpmgcl  31429  cyc3conja  31433  rhmopp  31527  nsgmgc  31606  nsgqusf1olem1  31607  nsgqusf1olem2  31608  rhmpreimaprmidl  31636  ssmxidllem  31650  fply1  31676  smatlem  31756  smatcl  31761  zartopn  31834  zarmxt1  31839  tpr2rico  31871  xrmulc1cn  31889  xrge0mulc1cn  31900  esumpfinvallem  32051  ldgenpisyslem1  32140  dynkin  32144  brfae  32225  sxbrsigalem3  32248  dya2icoseg2  32254  omsmeas  32299  sibfof  32316  sseqmw  32367  sseqf  32368  sseqp1  32371  fiblem  32374  fibp1  32377  probfinmeasbALTV  32405  repr0  32600  reprpmtf1o  32615  hgt750lemg  32643  bnj1379  32819  srcmpltd  33063  subfacp1lem5  33155  subfacp1lem6  33156  cvxpconn  33213  cvxsconn  33214  cvmliftlem6  33261  cvmliftlem8  33263  cvmliftlem10  33265  cvmlift2lem6  33279  cvmlift2lem11  33284  cvmlift2lem12  33285  2goelgoanfmla1  33395  prv1n  33402  msubff  33501  msubco  33502  elmsta  33519  msubff1  33527  mvhf  33529  msubvrs  33531  iprodefisumlem  33715  filnetlem3  34578  knoppcnlem10  34691  knoppcnlem11  34692  icoreunrn  35539  icoreelrn  35541  ralssiun  35587  poimirlem3  35789  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem30  35816  dvasin  35870  cover2  35881  upixp  35896  sdclem1  35910  fdc  35912  caushft  35928  ismtyres  35975  rrncmslem  35999  isfld2  36172  osumcllem10N  37986  pexmidlem7N  37997  dihglblem2N  39315  lcfrvalsnN  39562  lcfrlem5  39567  lcfrlem6  39568  lcfrlem27  39590  lcfrlem37  39600  prjspvs  40456  0prjspnrel  40471  monotuz  40770  expdiophlem1  40850  kelac2  40897  grurankcld  41858  dvgrat  41937  nzss  41942  uzmptshftfval  41971  binomcxplemnotnn0  41981  refsumcn  42580  rfcnpre2  42581  rfcnpre3  42583  rfcnpre4  42584  elabrexg  42596  disjf1o  42736  unirnmap  42755  unirnmapsn  42761  ssmapsn  42763  mptssid  42792  allbutfi  42940  eluzd  42956  uzidd2  42963  ressiocsup  43099  ressioosup  43100  ressiooinf  43102  fsumsermpt  43127  climexp  43153  climinf  43154  climsuse  43156  sumnnodd  43178  limsupresico  43248  limsupubuzlem  43260  limsupresxr  43314  liminfresxr  43315  liminfresico  43319  limsup10exlem  43320  cnrefiisplem  43377  cncfiooicclem1  43441  dvsinax  43461  itgsinexplem1  43502  fvvolioof  43537  fvvolicof  43539  stoweidlem14  43562  stoweidlem16  43564  stoweidlem31  43579  stoweidlem34  43582  stoweidlem36  43584  stoweidlem43  43591  stoweidlem46  43594  stoweidlem47  43595  stoweidlem52  43600  stoweidlem55  43603  stoweidlem57  43605  dirkercncf  43655  fourierdlem20  43675  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem51  43705  fourierdlem54  43708  fourierdlem62  43716  fourierdlem71  43725  fourierdlem80  43734  fourierdlem114  43768  fouriersw  43779  ioorrnopnlem  43852  ioorrnopnxrlem  43854  salexct3  43888  salgencntex  43889  salgensscntex  43890  subsalsal  43905  sge0fodjrnlem  43961  sge0isum  43972  sge0seq  43991  sge0reuz  43992  sge0reuzb  43993  meadjiunlem  44010  meaiininclem  44031  carageniuncllem1  44066  caratheodorylem1  44071  hoiprodp1  44133  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  voncmpl  44166  hoiqssbl  44170  smflimlem2  44317  smfsuplem1  44355  smfsuplem3  44357  cfsetsnfsetf  44563  fcores  44572  afvres  44675  afv2res  44742  fundcmpsurinjimaid  44874  iccpartigtl  44886  sprsymrelf  44958  prproropf1olem2  44967  ushrisomgr  45304  funcringcsetcALTV2lem3  45607  funcringcsetclem3ALTV  45630  lindslinindsimp2lem5  45814  rrxsphere  46105  line2  46109  iooii  46222  icccldii  46223  iscnrm3rlem3  46247  onsetreclem3  46423  amgmwlem  46517