Theorem eleqtrrid 2859

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
eleqtrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrid

Step	Hyp	Ref	Expression
1		eleqtrrid.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2764	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrid 2858	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830

This theorem is referenced by:  rabsnt  4627  onnev  6295  onnevOLD  6296  opabiota  6740  canth  7111  onnseq  7997  tfrlem16  8045  oen0  8228  nnawordex  8279  inf0  9130  cantnflt  9181  cnfcom2  9211  cnfcom3lem  9212  cnfcom3  9213  r1ordg  9253  r1val1  9261  rankr1id  9337  acacni  9613  dfacacn  9614  dfac13  9615  ttukeylem5  9986  ttukeylem6  9987  gch2  10148  gch3  10149  gchac  10154  gchina  10172  swrds1  14088  wrdl3s3  14386  sadcp1  15867  lcmfunsnlem2  16050  fnpr2ob  16903  idfucl  17224  gsumval2  17976  gsumz  18080  frmdmnd  18104  frmd0  18105  efginvrel2  18934  efgcpbl2  18964  pgpfaclem1  19285  lbsexg  20018  zringndrg  20272  frlmlbs  20576  mat0dimscm  21183  mat0scmat  21252  m2detleiblem5  21339  m2detleiblem6  21340  m2detleiblem3  21343  m2detleiblem4  21344  d0mat2pmat  21452  chpmat0d  21548  dfac14  22332  acufl  22631  cnextfvval  22779  cnextcn  22781  minveclem3b  24142  minveclem4a  24144  ovollb2  24203  ovolunlem1a  24210  ovolunlem1  24211  ovoliunlem1  24216  ovoliun2  24220  ioombl1lem4  24275  uniioombllem1  24295  uniioombllem2  24297  uniioombllem6  24302  itg2monolem1  24464  itg2mono  24467  itg2cnlem1  24475  xrlimcnp  25667  efrlim  25668  eengbas  26888  ebtwntg  26889  ecgrtg  26890  elntg  26891  wlkl1loop  27540  elwwlks2ons3im  27853  upgr3v3e3cycl  28078  upgr4cycl4dv4e  28083  2clwwlk2clwwlk  28248  ex-br  28329  trsp2cyc  30929  cyc3evpm  30956  lvecdim0  31224  extdg1id  31272  rge0scvg  31433  repr0  32123  hgt750lemg  32166  mrsub0  33007  elmrsubrn  33011  topjoin  34138  finorwe  35114  pclfinN  37511  aomclem1  40416  dfac21  40428  clsk1indlem1  41166  mnurndlem1  41407  fourierdlem102  43261  fourierdlem114  43273  lincval0  45248  lcoel0  45261