Theorem eleqtrrid 2843

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

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

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 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  rabsnt  4688  onnev  6445  opabiota  6916  canth  7312  onnseq  8276  tfrlem16  8324  oen0  8514  nnawordex  8565  inf0  9530  cantnflt  9581  cnfcom2  9611  cnfcom3lem  9612  cnfcom3  9613  r1ordg  9690  r1val1  9698  rankr1id  9774  acacni  10051  dfacacn  10052  dfac13  10053  ttukeylem5  10423  ttukeylem6  10424  gch2  10586  gch3  10587  gchac  10592  gchina  10610  swrds1  14590  wrdl3s3  14885  sadcp1  16382  lcmfunsnlem2  16567  fnpr2ob  17479  idfucl  17805  gsumval2  18611  gsumz  18761  frmdmnd  18784  frmd0  18785  efginvrel2  19656  efgcpbl2  19686  pgpfaclem1  20012  lbsexg  21119  zringndrg  21423  frlmlbs  21752  mat0dimscm  22413  mat0scmat  22482  m2detleiblem5  22569  m2detleiblem6  22570  m2detleiblem3  22573  m2detleiblem4  22574  d0mat2pmat  22682  chpmat0d  22778  dfac14  23562  acufl  23861  cnextfvval  24009  cnextcn  24011  minveclem3b  25384  minveclem4a  25386  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun2  25463  ioombl1lem4  25518  uniioombllem1  25538  uniioombllem2  25540  uniioombllem6  25545  itg2monolem1  25707  itg2mono  25710  itg2cnlem1  25718  xrlimcnp  26934  efrlim  26935  efrlimOLD  26936  eengbas  29054  ebtwntg  29055  ecgrtg  29056  elntg  29057  wlkl1loop  29711  elwwlks2ons3im  30027  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  2clwwlk2clwwlk  30425  ex-br  30506  trsp2cyc  33205  cyc3evpm  33232  ply1dg1rtn0  33662  lvecdim0  33763  extdg1id  33823  irngss  33844  rge0scvg  34106  repr0  34768  hgt750lemg  34811  r1wf  35252  mrsub0  35710  elmrsubrn  35714  topjoin  36559  finorwe  37587  pclfinN  40160  aomclem1  43296  dfac21  43308  naddgeoa  43636  clsk1indlem1  44286  mnurndlem1  44522  fourierdlem102  46452  fourierdlem114  46464  cycl3grtri  48193  lincval0  48661  lcoel0  48674  discsubc  49309  prsthinc  49709  isinito2lem  49743  termcarweu  49773  diag1f1o  49779  diag2f1o  49782  initocmd  49914