Theorem eleqtrrdi 2924

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  3eltr4g  2930  brelrng  5811  elabrex  7002  fliftel1  7063  ovidig  7292  unielxp  7727  tfrlem11  8024  rdglim  8062  seqomlem4  8089  2oconcl  8128  ecopqsi  8354  erov  8394  eroprf  8395  sbthlem2  8628  dffi3  8895  ixpiunwdom  9055  cantnfcl  9130  r1lim  9201  rankwflemb  9222  pwwf  9236  unwf  9239  rankwflem  9244  uniwf  9248  rankpwi  9252  rankr1g  9261  r1pw  9274  r1rankid  9288  rankuni  9292  djulcl  9339  djurcl  9340  inlresf  9343  inrresf  9345  djuun  9355  cardlim  9401  infxpenlem  9439  alephfp  9534  cfsmolem  9692  alephsing  9698  hsmexlem4  9851  axdc3lem2  9873  numth3  9892  iunfo  9961  konigthlem  9990  iunctb  9996  canthwelem  10072  canthwe  10073  r1limwun  10158  inar1  10197  inatsk  10200  gruina  10240  grur1  10242  tskmval  10261  tskmcl  10263  pinq  10349  dmrecnq  10390  addclsr  10505  mulclsr  10506  axaddf  10567  axmulf  10568  peano2nn  11650  uztrn2  12263  eluz2nn  12285  peano2uzs  12303  uzsupss  12341  uzsup  13232  uzrdgfni  13327  uzrdgsuci  13329  fsuppmapnn0fiub  13360  seqf  13392  ser0  13423  bcm1k  13676  bcp1nk  13678  bcpasc  13682  hashprdifel  13760  fz1isolem  13820  pr2pwpr  13838  ccats1val2  13983  rexuzre  14712  limsupgre  14838  climconst  14900  rlimclim1  14902  climrlim2  14904  clim2ser  15011  clim2ser2  15012  iserex  15013  isermulc2  15014  iserle  15016  isercolllem3  15023  isercoll2  15025  climsup  15026  iseraltlem2  15039  iseraltlem3  15040  zsum  15075  isumclim3  15114  isumadd  15122  fsump1i  15124  iserabs  15170  cvgcmp  15171  cvgcmpub  15172  cvgcmpce  15173  abscvgcvg  15174  isumshft  15194  isumsplit  15195  isum1p  15196  isumrpcl  15198  isumsup2  15201  climcndslem1  15204  cvgrat  15239  clim2prod  15244  clim2div  15245  prodf1  15247  ntrivcvgn0  15254  ntrivcvgtail  15256  fprodntriv  15296  fprodabs  15328  fprodeq0  15329  iprodclim3  15354  iprodmul  15357  ef0lem  15432  fprodefsum  15448  rpnnen2lem3  15569  dvdsflip  15667  fzo0dvdseq  15673  bitsinv1  15791  smupval  15837  smueqlem  15839  seq1st  15915  algr0  15916  prmind2  16029  crth  16115  eulerthlem2  16119  prmdiv  16122  pockthlem  16241  pockthg  16242  unbenlem  16244  prmunb  16250  prmgaplem7  16393  strfv2d  16529  imasvscaval  16811  oppccatid  16989  epii  17013  fthepi  17198  funcestrcsetclem3  17392  funcsetcestrclem3  17406  yon12  17515  yon2  17516  yonedalem4c  17527  yonedalem22  17528  yonedalem3b  17529  yonedainv  17531  acsmapd  17788  mgm2nsgrplem1  18083  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  sgrp2nmndlem1  18088  sgrp2rid2  18091  cntrsubgnsg  18471  symgpssefmnd  18524  pmtrrn  18585  gexcl3  18712  efgi  18845  efgi2  18851  efgs1b  18862  efgredlemg  18868  efgredlemd  18870  frgpnabllem1  18993  cycsubgcyg  19021  gsumzaddlem  19041  dprdwd  19133  dprd2da  19164  lsppratlem3  19921  lsppratlem4  19922  lbsextlem2  19931  lidl0  19992  lidl1  19993  mplsubrglem  20219  mpfconst  20314  mpfproj  20315  mpfind  20320  pf1const  20509  pf1id  20510  mpfpf1  20514  pf1mpf  20515  domnchr  20679  znf1o  20698  madetsumid  21070  slesolex  21291  pmatcoe1fsupp  21309  mat2pmatbas0  21335  pmatcollpw  21389  pm2mpf1  21407  isclo  21695  indiscld  21699  restntr  21790  ordtbaslem  21796  ordtbas2  21799  lmconst  21869  lmss  21906  conncompid  22039  2ndcomap  22066  locfincmp  22134  comppfsc  22140  xkouni  22207  txcls  22212  ptclsg  22223  uptx  22233  txindis  22242  tx1stc  22258  cnmpt1res  22284  tgqtop  22320  uffix  22529  cnpflf2  22608  ptcmplem2  22661  ptcmplem4  22663  tgpconncomp  22721  tsmsfbas  22736  fmucnd  22901  prdsxmetlem  22978  imasdsf1olem  22983  prdsbl  23101  blcvx  23406  xrsmopn  23420  xrge0tsms  23442  metdcn2  23447  expcncf  23530  cnmpopc  23532  icchmeo  23545  iccpnfhmeo  23549  cnheibor  23559  evth  23563  evth2  23564  lebnumlem2  23566  lebnumii  23570  reparphti  23601  cfilfcls  23877  minveclem2  24029  minveclem3  24032  minveclem4  24035  ovoliunlem1  24103  ovolicc1  24117  iundisj  24149  volsup  24157  uniioombllem3  24186  vitalilem2  24210  vitalilem3  24211  mbfsup  24265  mbfinf  24266  mbflimsup  24267  itg2monolem1  24351  limcflflem  24478  limccnp  24489  limccnp2  24490  dvidlem  24513  dvn2bss  24527  cpnres  24534  dvcobr  24543  dvrec  24552  c1liplem1  24593  dvcnvrelem2  24615  dvfsumrlimf  24622  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlim  24628  dvfsum2  24631  coeeulem  24814  coeid3  24830  plycn  24851  dvntaylp  24959  taylthlem1  24961  taylthlem2  24962  ulm2  24973  ulmshftlem  24977  ulmshft  24978  ulm0  24979  ulmcn  24987  ulmdvlem3  24990  ulmdv  24991  mtest  24992  mtestbdd  24993  dvradcnv  25009  psercn2  25011  psercn  25014  pserdv  25017  abelth  25029  efif1olem2  25127  efif1olem4  25129  efifo  25131  eff1olem  25132  logcn  25230  dvloglem  25231  cxpcn3  25329  resqrtcn  25330  sqrtcn  25331  logbleb  25361  logblt  25362  asinneg  25464  atanlogsub  25494  atanbnd  25504  ressatans  25512  leibpilem2  25519  xrlimcnp  25546  efrlim  25547  scvxcvx  25563  ppiub  25780  chtub  25788  logexprlim  25801  lgseisenlem1  25951  rplogsumlem1  26060  rplogsumlem2  26061  dchrisumlem2  26066  dchrisum0flb  26086  logdivbnd  26132  pntlem3  26185  tgcgr4  26317  ltgov  26383  f1otrg  26657  eengtrkg  26772  iedgedg  26835  ushgredgedgloop  27013  subgruhgredgd  27066  uvtxupgrres  27190  umgr2v2evd2  27309  edginwlk  27416  wlk1walk  27420  crctcshwlkn0lem6  27593  wlkiswwlks1  27645  minvecolem1  28651  minvecolem2  28652  minvecolem4  28657  htthlem  28694  5oalem2  29432  3oalem2  29440  iundisjf  30339  fmptco1f1o  30378  xppreima  30394  xppreima2  30395  dfcnv2  30422  xrge0tsmsd  30692  odpmco  30730  pmtrcnelor  30735  pmtrto1cl  30741  psgnfzto1stlem  30742  fzto1stfv1  30743  fzto1st  30745  fzto1stinvn  30746  psgnfzto1st  30747  tocycf  30759  cycpmco2lem7  30774  cycpmco2  30775  cycpmrn  30785  cyc3evpm  30792  cyc3genpmlem  30793  cycpmgcl  30795  cyc3conja  30799  rhmopp  30892  fply1  30931  ssmxidllem  30978  smatlem  31062  smatcl  31067  tpr2rico  31155  xrmulc1cn  31173  xrge0mulc1cn  31184  esumpfinvallem  31333  ldgenpisyslem1  31422  dynkin  31426  brfae  31507  sxbrsigalem3  31530  dya2icoseg2  31536  omsmeas  31581  sibfof  31598  sseqmw  31649  sseqf  31650  sseqp1  31653  fiblem  31656  fibp1  31659  probfinmeasbALTV  31687  repr0  31882  reprpmtf1o  31897  hgt750lemg  31925  bnj1379  32102  srcmpltd  32346  subfacp1lem5  32431  subfacp1lem6  32432  cvxpconn  32489  cvxsconn  32490  cvmliftlem6  32537  cvmliftlem8  32539  cvmliftlem10  32541  cvmlift2lem6  32555  cvmlift2lem11  32560  cvmlift2lem12  32561  2goelgoanfmla1  32671  prv1n  32678  msubff  32777  msubco  32778  elmsta  32795  msubff1  32803  mvhf  32805  msubvrs  32807  iprodefisumlem  32972  filnetlem3  33728  knoppcnlem10  33841  knoppcnlem11  33842  icoreunrn  34643  icoreelrn  34645  ralssiun  34691  poimirlem3  34910  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem30  34937  dvasin  34993  cover2  35004  upixp  35019  sdclem1  35033  fdc  35035  caushft  35051  ismtyres  35101  rrncmslem  35125  isfld2  35298  osumcllem10N  37116  pexmidlem7N  37127  dihglblem2N  38445  lcfrvalsnN  38692  lcfrlem5  38697  lcfrlem6  38698  lcfrlem27  38720  lcfrlem37  38730  prjspvs  39309  0prjspnrel  39318  monotuz  39587  expdiophlem1  39667  kelac2  39714  grurankcld  40618  dvgrat  40693  nzss  40698  uzmptshftfval  40727  binomcxplemnotnn0  40737  refsumcn  41336  rfcnpre2  41337  rfcnpre3  41339  rfcnpre4  41340  elabrexg  41352  disjf1o  41501  unirnmap  41520  unirnmapsn  41526  ssmapsn  41528  mptssid  41560  allbutfi  41714  eluzd  41731  uzidd2  41739  ressiocsup  41879  ressioosup  41880  ressiooinf  41882  fsumsermpt  41909  climexp  41935  climinf  41936  climsuse  41938  sumnnodd  41960  limsupresico  42030  limsupubuzlem  42042  limsupresxr  42096  liminfresxr  42097  liminfresico  42101  limsup10exlem  42102  cnrefiisplem  42159  cncfiooicclem1  42225  dvsinax  42246  itgsinexplem1  42288  fvvolioof  42323  fvvolicof  42325  stoweidlem14  42348  stoweidlem16  42350  stoweidlem31  42365  stoweidlem34  42368  stoweidlem36  42370  stoweidlem43  42377  stoweidlem46  42380  stoweidlem47  42381  stoweidlem52  42386  stoweidlem55  42389  stoweidlem57  42391  dirkercncf  42441  fourierdlem20  42461  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem51  42491  fourierdlem54  42494  fourierdlem62  42502  fourierdlem71  42511  fourierdlem80  42520  fourierdlem114  42554  fouriersw  42565  ioorrnopnlem  42638  ioorrnopnxrlem  42640  salexct3  42674  salgencntex  42675  salgensscntex  42676  subsalsal  42691  sge0fodjrnlem  42747  sge0isum  42758  sge0seq  42777  sge0reuz  42778  sge0reuzb  42779  meadjiunlem  42796  meaiininclem  42817  carageniuncllem1  42852  caratheodorylem1  42857  hoiprodp1  42919  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  voncmpl  42952  hoiqssbl  42956  smflimlem2  43097  smfsuplem1  43134  smfsuplem3  43136  afvres  43420  afv2res  43487  fundcmpsurinjimaid  43620  iccpartigtl  43632  sprsymrelf  43706  prproropf1olem2  43715  ushrisomgr  44055  funcringcsetcALTV2lem3  44358  funcringcsetclem3ALTV  44381  lindslinindsimp2lem5  44566  rrxsphere  44784  line2  44788  onsetreclem3  44858  amgmwlem  44952