Theorem eleqtrrid 2851

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  rabsnt  4756  onnev  6522  opabiota  7004  canth  7401  onnseq  8400  tfrlem16  8449  oen0  8642  nnawordex  8693  inf0  9690  cantnflt  9741  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  r1ordg  9847  r1val1  9855  rankr1id  9931  acacni  10210  dfacacn  10211  dfac13  10212  ttukeylem5  10582  ttukeylem6  10583  gch2  10744  gch3  10745  gchac  10750  gchina  10768  swrds1  14714  wrdl3s3  15011  sadcp1  16501  lcmfunsnlem2  16687  fnpr2ob  17618  idfucl  17945  gsumval2  18724  gsumz  18871  frmdmnd  18894  frmd0  18895  efginvrel2  19769  efgcpbl2  19799  pgpfaclem1  20125  lbsexg  21189  zringndrg  21502  frlmlbs  21840  mat0dimscm  22496  mat0scmat  22565  m2detleiblem5  22652  m2detleiblem6  22653  m2detleiblem3  22656  m2detleiblem4  22657  d0mat2pmat  22765  chpmat0d  22861  dfac14  23647  acufl  23946  cnextfvval  24094  cnextcn  24096  minveclem3b  25481  minveclem4a  25483  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem6  25642  itg2monolem1  25805  itg2mono  25808  itg2cnlem1  25816  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  eengbas  29014  ebtwntg  29015  ecgrtg  29016  elntg  29017  wlkl1loop  29674  elwwlks2ons3im  29987  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  2clwwlk2clwwlk  30382  ex-br  30463  trsp2cyc  33116  cyc3evpm  33143  ply1dg1rtn0  33570  lvecdim0  33619  extdg1id  33676  irngss  33687  rge0scvg  33895  repr0  34588  hgt750lemg  34631  mrsub0  35484  elmrsubrn  35488  topjoin  36331  finorwe  37348  pclfinN  39857  aomclem1  43011  dfac21  43023  naddgeoa  43356  clsk1indlem1  44007  mnurndlem1  44250  fourierdlem102  46129  fourierdlem114  46141  lincval0  48144  lcoel0  48157  prsthinc  48721