Theorem syl5eleqr 2695

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl5eleqr.1	⊢ 𝐴 ∈ 𝐵
syl5eleqr.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
syl5eleqr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl5eleqr

Step	Hyp	Ref	Expression
1		syl5eleqr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		syl5eleqr.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2616	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	syl5eleq 2694	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  rabsnt  4210  onnev  5765  opabiota  6171  canth  6508  onnseq  7328  tfrlem16  7376  oen0  7553  nnawordex  7604  inf0  8401  cantnflt  8452  cnfcom2  8482  cnfcom3lem  8483  cnfcom3  8484  r1ordg  8524  r1val1  8532  rankr1id  8608  acacni  8845  dfacacn  8846  dfac13  8847  cda1dif  8881  ttukeylem5  9218  ttukeylem6  9219  gch2  9376  gch3  9377  gchac  9382  gchina  9400  swrds1  13303  wrdl3s3  13553  sadcp1  15015  lcmfunsnlem2  15191  xpsfrnel2  16048  idfucl  16364  gsumval2  17103  gsumz  17197  frmdmnd  17219  frmd0  17220  efginvrel2  17963  efgcpbl2  17993  pgpfaclem1  18303  lbsexg  18985  zringndrg  19657  frlmlbs  19955  mat0dimscm  20094  mat0scmat  20163  m2detleiblem5  20250  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  d0mat2pmat  20362  chpmat0d  20458  dfac14  21231  acufl  21531  cnextfvval  21679  cnextcn  21681  minveclem3b  23007  minveclem4a  23009  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun2  23081  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem2  23157  uniioombllem6  23162  itg2monolem1  23323  itg2mono  23326  itg2cnlem1  23334  xrlimcnp  24495  efrlim  24496  eengbas  25661  ebtwntg  25662  ecgrtg  25663  elntg  25664  cusgrares  26001  usgrcyclnl1  26168  ex-br  26680  rge0scvg  29323  mrsub0  30667  elmrsubrn  30671  topjoin  31530  pclfinN  34204  aomclem1  36642  dfac21  36654  clsk1indlem1  37363  fourierdlem102  39101  fourierdlem114  39113  1wlkl1loop  40842  wwlks2onv  41158  elwwlks2ons3  41159  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  lincval0  41998  lcoel0  42011