Theorem eleqtrrid 2848

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  rabsnt  4731  onnev  6511  opabiota  6991  canth  7385  onnseq  8384  tfrlem16  8433  oen0  8624  nnawordex  8675  inf0  9661  cantnflt  9712  cnfcom2  9742  cnfcom3lem  9743  cnfcom3  9744  r1ordg  9818  r1val1  9826  rankr1id  9902  acacni  10181  dfacacn  10182  dfac13  10183  ttukeylem5  10553  ttukeylem6  10554  gch2  10715  gch3  10716  gchac  10721  gchina  10739  swrds1  14704  wrdl3s3  15001  sadcp1  16492  lcmfunsnlem2  16677  fnpr2ob  17603  idfucl  17926  gsumval2  18699  gsumz  18849  frmdmnd  18872  frmd0  18873  efginvrel2  19745  efgcpbl2  19775  pgpfaclem1  20101  lbsexg  21166  zringndrg  21479  frlmlbs  21817  mat0dimscm  22475  mat0scmat  22544  m2detleiblem5  22631  m2detleiblem6  22632  m2detleiblem3  22635  m2detleiblem4  22636  d0mat2pmat  22744  chpmat0d  22840  dfac14  23626  acufl  23925  cnextfvval  24073  cnextcn  24075  minveclem3b  25462  minveclem4a  25464  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun2  25541  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  itg2monolem1  25785  itg2mono  25788  itg2cnlem1  25796  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  eengbas  28996  ebtwntg  28997  ecgrtg  28998  elntg  28999  wlkl1loop  29656  elwwlks2ons3im  29974  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  2clwwlk2clwwlk  30369  ex-br  30450  trsp2cyc  33143  cyc3evpm  33170  ply1dg1rtn0  33605  lvecdim0  33657  extdg1id  33716  irngss  33737  rge0scvg  33948  repr0  34626  hgt750lemg  34669  mrsub0  35521  elmrsubrn  35525  topjoin  36366  finorwe  37383  pclfinN  39902  aomclem1  43066  dfac21  43078  naddgeoa  43407  clsk1indlem1  44058  mnurndlem1  44300  fourierdlem102  46223  fourierdlem114  46235  cycl3grtri  47914  lincval0  48332  lcoel0  48345  prsthinc  49111