Theorem eleqtrrid 2838

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

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

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  rabsnt  4681  onnev  6434  opabiota  6904  canth  7300  onnseq  8264  tfrlem16  8312  oen0  8501  nnawordex  8552  inf0  9511  cantnflt  9562  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  r1ordg  9671  r1val1  9679  rankr1id  9755  acacni  10032  dfacacn  10033  dfac13  10034  ttukeylem5  10404  ttukeylem6  10405  gch2  10566  gch3  10567  gchac  10572  gchina  10590  swrds1  14574  wrdl3s3  14869  sadcp1  16366  lcmfunsnlem2  16551  fnpr2ob  17462  idfucl  17788  gsumval2  18594  gsumz  18744  frmdmnd  18767  frmd0  18768  efginvrel2  19639  efgcpbl2  19669  pgpfaclem1  19995  lbsexg  21101  zringndrg  21405  frlmlbs  21734  mat0dimscm  22384  mat0scmat  22453  m2detleiblem5  22540  m2detleiblem6  22541  m2detleiblem3  22544  m2detleiblem4  22545  d0mat2pmat  22653  chpmat0d  22749  dfac14  23533  acufl  23832  cnextfvval  23980  cnextcn  23982  minveclem3b  25355  minveclem4a  25357  ovollb2  25417  ovolunlem1a  25424  ovolunlem1  25425  ovoliunlem1  25430  ovoliun2  25434  ioombl1lem4  25489  uniioombllem1  25509  uniioombllem2  25511  uniioombllem6  25516  itg2monolem1  25678  itg2mono  25681  itg2cnlem1  25689  xrlimcnp  26905  efrlim  26906  efrlimOLD  26907  eengbas  28959  ebtwntg  28960  ecgrtg  28961  elntg  28962  wlkl1loop  29616  elwwlks2ons3im  29932  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  2clwwlk2clwwlk  30330  ex-br  30411  trsp2cyc  33092  cyc3evpm  33119  ply1dg1rtn0  33544  lvecdim0  33619  extdg1id  33679  irngss  33700  rge0scvg  33962  repr0  34624  hgt750lemg  34667  r1wf  35107  mrsub0  35560  elmrsubrn  35564  topjoin  36409  finorwe  37426  pclfinN  40009  aomclem1  43157  dfac21  43169  naddgeoa  43497  clsk1indlem1  44148  mnurndlem1  44384  fourierdlem102  46316  fourierdlem114  46328  cycl3grtri  48057  lincval0  48526  lcoel0  48539  discsubc  49175  prsthinc  49575  isinito2lem  49609  termcarweu  49639  diag1f1o  49645  diag2f1o  49648  initocmd  49780