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  4691  onnev  6449  opabiota  6925  canth  7323  onnseq  8290  tfrlem16  8338  oen0  8527  nnawordex  8578  inf0  9550  cantnflt  9601  cnfcom2  9631  cnfcom3lem  9632  cnfcom3  9633  r1ordg  9707  r1val1  9715  rankr1id  9791  acacni  10070  dfacacn  10071  dfac13  10072  ttukeylem5  10442  ttukeylem6  10443  gch2  10604  gch3  10605  gchac  10610  gchina  10628  swrds1  14607  wrdl3s3  14904  sadcp1  16401  lcmfunsnlem2  16586  fnpr2ob  17497  idfucl  17823  gsumval2  18595  gsumz  18745  frmdmnd  18768  frmd0  18769  efginvrel2  19641  efgcpbl2  19671  pgpfaclem1  19997  lbsexg  21106  zringndrg  21410  frlmlbs  21739  mat0dimscm  22389  mat0scmat  22458  m2detleiblem5  22545  m2detleiblem6  22546  m2detleiblem3  22549  m2detleiblem4  22550  d0mat2pmat  22658  chpmat0d  22754  dfac14  23538  acufl  23837  cnextfvval  23985  cnextcn  23987  minveclem3b  25361  minveclem4a  25363  ovollb2  25423  ovolunlem1a  25430  ovolunlem1  25431  ovoliunlem1  25436  ovoliun2  25440  ioombl1lem4  25495  uniioombllem1  25515  uniioombllem2  25517  uniioombllem6  25522  itg2monolem1  25684  itg2mono  25687  itg2cnlem1  25695  xrlimcnp  26911  efrlim  26912  efrlimOLD  26913  eengbas  28961  ebtwntg  28962  ecgrtg  28963  elntg  28964  wlkl1loop  29618  elwwlks2ons3im  29934  upgr3v3e3cycl  30159  upgr4cycl4dv4e  30164  2clwwlk2clwwlk  30329  ex-br  30410  trsp2cyc  33095  cyc3evpm  33122  ply1dg1rtn0  33542  lvecdim0  33595  extdg1id  33654  irngss  33675  rge0scvg  33932  repr0  34595  hgt750lemg  34638  mrsub0  35496  elmrsubrn  35500  topjoin  36346  finorwe  37363  pclfinN  39887  aomclem1  43036  dfac21  43048  naddgeoa  43376  clsk1indlem1  44027  mnurndlem1  44263  fourierdlem102  46199  fourierdlem114  46211  cycl3grtri  47939  lincval0  48397  lcoel0  48410  discsubc  49046  prsthinc  49446  isinito2lem  49480  termcarweu  49510  diag1f1o  49516  diag2f1o  49519  initocmd  49651