Theorem eleqtrrid 2870

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  rabsnt  4697  onnev  6489  opabiota  6963  canth  7364  onnseq  8327  tfrlem16  8376  oen0  8568  nnawordex  8619  inf0  9586  cantnflt  9637  cnfcom2  9667  cnfcom3lem  9668  cnfcom3  9669  r1ordg  9746  r1val1  9754  rankr1id  9830  acacni  10120  dfacacn  10121  dfac13  10122  ttukeylem5  10492  ttukeylem6  10493  gch2  10655  gch3  10656  gchac  10661  gchina  10679  swrds1  14700  wrdl3s3  14995  sadcp1  16508  lcmfunsnlem2  16693  fnpr2ob  17607  idfucl  17933  gsumval2  18739  gsumz  18890  frmdmnd  18913  frmd0  18914  efginvrel2  19792  efgcpbl2  19822  pgpfaclem1  20148  lbsexg  21288  zringndrg  21618  frlmlbs  21947  mat0dimscm  22626  mat0scmat  22695  m2detleiblem5  22782  m2detleiblem6  22783  m2detleiblem3  22786  m2detleiblem4  22787  d0mat2pmat  22895  chpmat0d  22991  dfac14  23775  acufl  24074  cnextfvval  24222  cnextcn  24224  minveclem3b  25587  minveclem4a  25589  ovollb2  25648  ovolunlem1a  25655  ovolunlem1  25656  ovoliunlem1  25661  ovoliun2  25665  ioombl1lem4  25720  uniioombllem1  25740  uniioombllem2  25742  uniioombllem6  25747  itg2monolem1  25909  itg2mono  25912  itg2cnlem1  25920  xrlimcnp  27133  efrlim  27134  eengbas  29331  ebtwntg  29332  ecgrtg  29333  elntg  29334  wlkl1loop  29987  elwwlks2ons3im  30303  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  2clwwlk2clwwlk  30701  ex-br  30782  trsp2cyc  33443  cyc3evpm  33470  dflring3  33787  ply1dg1rtn0  33871  lvecdim0  33997  extdg1id  34056  irngss  34077  rge0scvg  34339  repr0  34998  hgt750lemg  35041  r1wf  35489  onvfowev  35600  mrsub0  36008  elmrsubrn  36012  topjoin  36876  finorwe  38028  pclfinN  40674  aomclem1  43781  dfac21  43793  naddgeoa  44121  clsk1indlem1  44771  mnurndlem1  44991  fourierdlem102  46922  fourierdlem114  46934  cycl3grtri  48712  lincval0  49195  lcoel0  49208  discsubc  49842  prsthinc  50242  isinito2lem  50276  termcarweu  50306  diag1f1o  50312  diag2f1o  50315  initocmd  50447