Theorem eleqtrrdi 2850

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

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

This theorem is referenced by:  3eltr4g  2856  brelrng  5852  elabrex  7118  fliftel1  7183  ovidig  7415  unielxp  7869  tfrlem11  8217  rdglim  8255  seqomlem4  8282  2oconcl  8331  ecopqsi  8561  erov  8601  eroprf  8602  sbthlem2  8869  dffi3  9188  ixpiunwdom  9347  cantnfcl  9423  r1lim  9528  rankwflemb  9549  pwwf  9563  unwf  9566  rankwflem  9571  uniwf  9575  rankpwi  9579  rankr1g  9588  r1pw  9601  r1rankid  9615  rankuni  9619  djulcl  9666  djurcl  9667  inlresf  9670  inrresf  9672  djuun  9682  cardlim  9728  infxpenlem  9767  alephfp  9862  cfsmolem  10024  alephsing  10030  hsmexlem4  10183  axdc3lem2  10205  numth3  10224  iunfo  10293  konigthlem  10322  iunctb  10328  canthwelem  10404  canthwe  10405  r1limwun  10490  inar1  10529  inatsk  10532  gruina  10572  grur1  10574  tskmval  10593  tskmcl  10595  pinq  10681  dmrecnq  10722  addclsr  10837  mulclsr  10838  axaddf  10899  axmulf  10900  peano2nn  11983  uztrn2  12599  eluz2nn  12622  peano2uzs  12640  uzsupss  12678  uzsup  13581  uzrdgfni  13676  uzrdgsuci  13678  fsuppmapnn0fiub  13709  seqf  13742  ser0  13773  bcm1k  14027  bcp1nk  14029  bcpasc  14033  hashprdifel  14111  fz1isolem  14173  pr2pwpr  14191  ccats1val2  14332  rexuzre  15062  limsupgre  15188  climconst  15250  rlimclim1  15252  climrlim2  15254  clim2ser  15364  clim2ser2  15365  iserex  15366  isermulc2  15367  iserle  15369  isercolllem3  15376  isercoll2  15378  climsup  15379  iseraltlem2  15392  iseraltlem3  15393  zsum  15428  isumclim3  15469  isumadd  15477  fsump1i  15479  iserabs  15525  cvgcmp  15526  cvgcmpub  15527  cvgcmpce  15528  abscvgcvg  15529  isumshft  15549  isumsplit  15550  isum1p  15551  isumrpcl  15553  isumsup2  15556  climcndslem1  15559  cvgrat  15593  clim2prod  15598  clim2div  15599  prodf1  15601  ntrivcvgn0  15608  ntrivcvgtail  15610  fprodntriv  15650  fprodabs  15682  fprodeq0  15683  iprodclim3  15708  iprodmul  15711  ef0lem  15786  fprodefsum  15802  rpnnen2lem3  15923  dvdsflip  16024  fzo0dvdseq  16030  bitsinv1  16147  smupval  16193  smueqlem  16195  seq1st  16274  algr0  16275  prmind2  16388  crth  16477  eulerthlem2  16481  prmdiv  16484  pockthlem  16604  pockthg  16605  unbenlem  16607  prmunb  16613  prmgaplem7  16756  strfv2d  16901  imasvscaval  17247  oppccatid  17428  oppccatf  17437  epii  17453  fthepi  17642  funcestrcsetclem3  17857  funcsetcestrclem3  17871  yon12  17981  yon2  17982  yonedalem4c  17993  yonedalem22  17994  yonedalem3b  17995  yonedainv  17997  acsmapd  18270  mgm2nsgrplem1  18555  mgm2nsgrplem2  18556  mgm2nsgrplem3  18557  sgrp2nmndlem1  18560  sgrp2rid2  18563  cntrsubgnsg  18945  symgpssefmnd  19001  pmtrrn  19063  gexcl3  19190  efgi  19323  efgi2  19329  efgs1b  19340  efgredlemg  19346  efgredlemd  19348  frgpnabllem1  19472  cycsubgcyg  19500  gsumzaddlem  19520  dprdwd  19612  dprd2da  19643  lsppratlem3  20409  lsppratlem4  20410  lbsextlem2  20419  lidl0  20488  lidl1  20489  domnchr  20734  znf1o  20757  mplsubrglem  21208  mpfconst  21309  mpfproj  21310  mpfind  21315  mhpmulcl  21337  pf1const  21510  pf1id  21511  mpfpf1  21515  pf1mpf  21516  madetsumid  21608  slesolex  21829  pmatcoe1fsupp  21848  mat2pmatbas0  21874  pmatcollpw  21928  pm2mpf1  21946  isclo  22236  indiscld  22240  restntr  22331  ordtbaslem  22337  ordtbas2  22340  lmconst  22410  lmss  22447  conncompid  22580  2ndcomap  22607  locfincmp  22675  comppfsc  22681  xkouni  22748  txcls  22753  ptclsg  22764  uptx  22774  txindis  22783  tx1stc  22799  cnmpt1res  22825  tgqtop  22861  uffix  23070  cnpflf2  23149  ptcmplem2  23202  ptcmplem4  23204  tgpconncomp  23262  tsmsfbas  23277  fmucnd  23442  prdsxmetlem  23519  imasdsf1olem  23524  prdsbl  23645  blcvx  23959  xrsmopn  23973  xrge0tsms  23995  metdcn2  24000  expcncf  24087  cnmpopc  24089  icchmeo  24102  iccpnfhmeo  24106  cnheibor  24116  evth  24120  evth2  24121  lebnumlem2  24123  lebnumii  24127  reparphti  24158  cfilfcls  24436  minveclem2  24588  minveclem3  24591  minveclem4  24594  ovoliunlem1  24664  ovolicc1  24678  iundisj  24710  volsup  24718  uniioombllem3  24747  vitalilem2  24771  vitalilem3  24772  mbfsup  24826  mbfinf  24827  mbflimsup  24828  itg2monolem1  24913  limcflflem  25042  limccnp  25053  limccnp2  25054  dvidlem  25077  dvn2bss  25092  cpnres  25099  dvcobr  25108  dvrec  25117  c1liplem1  25158  dvcnvrelem2  25180  dvfsumrlimf  25187  dvfsumlem1  25188  dvfsumlem2  25189  dvfsumlem3  25190  dvfsumlem4  25191  dvfsumrlim  25193  dvfsum2  25196  coeeulem  25383  coeid3  25399  plycn  25420  dvntaylp  25528  taylthlem1  25530  taylthlem2  25531  ulm2  25542  ulmshftlem  25546  ulmshft  25547  ulm0  25548  ulmcn  25556  ulmdvlem3  25559  ulmdv  25560  mtest  25561  mtestbdd  25562  dvradcnv  25578  psercn2  25580  psercn  25583  pserdv  25586  abelth  25598  efif1olem2  25697  efif1olem4  25699  efifo  25701  eff1olem  25702  logcn  25800  dvloglem  25801  cxpcn3  25899  resqrtcn  25900  sqrtcn  25901  logbleb  25931  logblt  25932  asinneg  26034  atanlogsub  26064  atanbnd  26074  ressatans  26082  leibpilem2  26089  xrlimcnp  26116  efrlim  26117  scvxcvx  26133  ppiub  26350  chtub  26358  logexprlim  26371  lgseisenlem1  26521  rplogsumlem1  26630  rplogsumlem2  26631  dchrisumlem2  26636  dchrisum0flb  26656  logdivbnd  26702  pntlem3  26755  tgcgr4  26890  ltgov  26956  f1otrg  27230  eengtrkg  27352  iedgedg  27418  ushgredgedgloop  27596  subgruhgredgd  27649  uvtxupgrres  27773  umgr2v2evd2  27892  edginwlk  28000  wlk1walk  28004  crctcshwlkn0lem6  28177  wlkiswwlks1  28229  minvecolem1  29233  minvecolem2  29234  minvecolem4  29239  htthlem  29276  5oalem2  30014  3oalem2  30022  iundisjf  30925  fmptco1f1o  30965  xppreima  30980  xppreima2  30985  dfcnv2  31010  gsumhashmul  31313  xrge0tsmsd  31314  odpmco  31352  pmtrcnelor  31357  pmtrto1cl  31363  psgnfzto1stlem  31364  fzto1stfv1  31365  fzto1st  31367  fzto1stinvn  31368  psgnfzto1st  31369  tocycf  31381  cycpmco2lem7  31396  cycpmco2  31397  cycpmrn  31407  cyc3evpm  31414  cyc3genpmlem  31415  cycpmgcl  31417  cyc3conja  31421  rhmopp  31515  nsgmgc  31594  nsgqusf1olem1  31595  nsgqusf1olem2  31596  rhmpreimaprmidl  31624  ssmxidllem  31638  fply1  31664  smatlem  31744  smatcl  31749  zartopn  31822  zarmxt1  31827  tpr2rico  31859  xrmulc1cn  31877  xrge0mulc1cn  31888  esumpfinvallem  32039  ldgenpisyslem1  32128  dynkin  32132  brfae  32213  sxbrsigalem3  32236  dya2icoseg2  32242  omsmeas  32287  sibfof  32304  sseqmw  32355  sseqf  32356  sseqp1  32359  fiblem  32362  fibp1  32365  probfinmeasbALTV  32393  repr0  32588  reprpmtf1o  32603  hgt750lemg  32631  bnj1379  32807  srcmpltd  33051  subfacp1lem5  33143  subfacp1lem6  33144  cvxpconn  33201  cvxsconn  33202  cvmliftlem6  33249  cvmliftlem8  33251  cvmliftlem10  33253  cvmlift2lem6  33267  cvmlift2lem11  33272  cvmlift2lem12  33273  2goelgoanfmla1  33383  prv1n  33390  msubff  33489  msubco  33490  elmsta  33507  msubff1  33515  mvhf  33517  msubvrs  33519  iprodefisumlem  33703  filnetlem3  34566  knoppcnlem10  34679  knoppcnlem11  34680  icoreunrn  35527  icoreelrn  35529  ralssiun  35575  poimirlem3  35777  poimirlem16  35790  poimirlem17  35791  poimirlem19  35793  poimirlem30  35804  dvasin  35858  cover2  35869  upixp  35884  sdclem1  35898  fdc  35900  caushft  35916  ismtyres  35963  rrncmslem  35987  isfld2  36160  osumcllem10N  37976  pexmidlem7N  37987  dihglblem2N  39305  lcfrvalsnN  39552  lcfrlem5  39557  lcfrlem6  39558  lcfrlem27  39580  lcfrlem37  39590  prjspvs  40446  0prjspnrel  40461  monotuz  40760  expdiophlem1  40840  kelac2  40887  grurankcld  41821  dvgrat  41900  nzss  41905  uzmptshftfval  41934  binomcxplemnotnn0  41944  refsumcn  42543  rfcnpre2  42544  rfcnpre3  42546  rfcnpre4  42547  elabrexg  42559  disjf1o  42699  unirnmap  42718  unirnmapsn  42724  ssmapsn  42726  mptssid  42755  allbutfi  42903  eluzd  42919  uzidd2  42926  ressiocsup  43062  ressioosup  43063  ressiooinf  43065  fsumsermpt  43090  climexp  43116  climinf  43117  climsuse  43119  sumnnodd  43141  limsupresico  43211  limsupubuzlem  43223  limsupresxr  43277  liminfresxr  43278  liminfresico  43282  limsup10exlem  43283  cnrefiisplem  43340  cncfiooicclem1  43404  dvsinax  43424  itgsinexplem1  43465  fvvolioof  43500  fvvolicof  43502  stoweidlem14  43525  stoweidlem16  43527  stoweidlem31  43542  stoweidlem34  43545  stoweidlem36  43547  stoweidlem43  43554  stoweidlem46  43557  stoweidlem47  43558  stoweidlem52  43563  stoweidlem55  43566  stoweidlem57  43568  dirkercncf  43618  fourierdlem20  43638  fourierdlem42  43660  fourierdlem48  43665  fourierdlem49  43666  fourierdlem51  43668  fourierdlem54  43671  fourierdlem62  43679  fourierdlem71  43688  fourierdlem80  43697  fourierdlem114  43731  fouriersw  43742  ioorrnopnlem  43815  ioorrnopnxrlem  43817  salexct3  43851  salgencntex  43852  salgensscntex  43853  subsalsal  43868  sge0fodjrnlem  43924  sge0isum  43935  sge0seq  43954  sge0reuz  43955  sge0reuzb  43956  meadjiunlem  43973  meaiininclem  43994  carageniuncllem1  44029  caratheodorylem1  44034  hoiprodp1  44096  hoidmv1lelem1  44099  hoidmv1lelem2  44100  hoidmv1le  44102  hoidmvlelem1  44103  hoidmvlelem2  44104  hoidmvlelem3  44105  voncmpl  44129  hoiqssbl  44133  smflimlem2  44274  smfsuplem1  44311  smfsuplem3  44313  cfsetsnfsetf  44519  fcores  44528  afvres  44631  afv2res  44698  fundcmpsurinjimaid  44830  iccpartigtl  44842  sprsymrelf  44914  prproropf1olem2  44923  ushrisomgr  45260  funcringcsetcALTV2lem3  45563  funcringcsetclem3ALTV  45586  lindslinindsimp2lem5  45770  rrxsphere  46061  line2  46065  iooii  46178  icccldii  46179  iscnrm3rlem3  46203  onsetreclem3  46379  amgmwlem  46473