Theorem eleqtrrid 2835

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  rabsnt  4695  onnev  6461  opabiota  6943  canth  7341  onnseq  8313  tfrlem16  8361  oen0  8550  nnawordex  8601  inf0  9574  cantnflt  9625  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  r1ordg  9731  r1val1  9739  rankr1id  9815  acacni  10094  dfacacn  10095  dfac13  10096  ttukeylem5  10466  ttukeylem6  10467  gch2  10628  gch3  10629  gchac  10634  gchina  10652  swrds1  14631  wrdl3s3  14928  sadcp1  16425  lcmfunsnlem2  16610  fnpr2ob  17521  idfucl  17843  gsumval2  18613  gsumz  18763  frmdmnd  18786  frmd0  18787  efginvrel2  19657  efgcpbl2  19687  pgpfaclem1  20013  lbsexg  21074  zringndrg  21378  frlmlbs  21706  mat0dimscm  22356  mat0scmat  22425  m2detleiblem5  22512  m2detleiblem6  22513  m2detleiblem3  22516  m2detleiblem4  22517  d0mat2pmat  22625  chpmat0d  22721  dfac14  23505  acufl  23804  cnextfvval  23952  cnextcn  23954  minveclem3b  25328  minveclem4a  25330  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun2  25407  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem2  25484  uniioombllem6  25489  itg2monolem1  25651  itg2mono  25654  itg2cnlem1  25662  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  eengbas  28908  ebtwntg  28909  ecgrtg  28910  elntg  28911  wlkl1loop  29566  elwwlks2ons3im  29884  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  2clwwlk2clwwlk  30279  ex-br  30360  trsp2cyc  33080  cyc3evpm  33107  ply1dg1rtn0  33549  lvecdim0  33602  extdg1id  33661  irngss  33682  rge0scvg  33939  repr0  34602  hgt750lemg  34645  mrsub0  35503  elmrsubrn  35507  topjoin  36353  finorwe  37370  pclfinN  39894  aomclem1  43043  dfac21  43055  naddgeoa  43383  clsk1indlem1  44034  mnurndlem1  44270  fourierdlem102  46206  fourierdlem114  46218  cycl3grtri  47946  lincval0  48404  lcoel0  48417  discsubc  49053  prsthinc  49453  isinito2lem  49487  termcarweu  49517  diag1f1o  49523  diag2f1o  49526  initocmd  49658