Theorem eqeltrrdi 2848

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrdi

Step	Hyp	Ref	Expression
1		eqeltrrdi.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2741	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrrdi.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	eqeltrdi 2847	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814

This theorem is referenced by:  axrep6g  5296  snexg  5441  wemoiso2  7998  releldm2  8067  mapprc  8869  mapfoss  8891  ixpprc  8958  bren  8994  brdomg  8996  brdomgOLD  8997  domssex  9177  mapen  9180  ssenen  9190  imafiOLD  9352  fodomfib  9367  fodomfibOLD  9369  fi0  9458  dffi3  9469  brwdom  9605  brwdomn0  9607  unxpwdom2  9626  ixpiunwdom  9628  tcmin  9779  rankonid  9867  rankr1id  9900  cardf2  9981  cardid2  9991  carduni  10019  fseqen  10065  acndom  10089  acndom2  10092  alephnbtwn  10109  cardcf  10290  cfeq0  10294  cflim2  10301  coftr  10311  infpssr  10346  hsmexlem5  10468  axdc3lem4  10491  fodomb  10564  ondomon  10601  gruina  10856  ioof  13484  hashbc  14489  trclun  15050  zsum  15751  fsum  15753  fprod  15974  eqgen  19212  symgfisg  19501  dvdsr  20379  asplss  21912  aspsubrg  21914  psrval  21953  clsf  23072  restco  23188  subbascn  23278  is2ndc  23470  ptbasin2  23602  ptbas  23603  indishmph  23822  ufldom  23986  cnextfres1  24092  ussid  24285  icopnfcld  24804  cnrehmeo  24998  cnrehmeoOLD  24999  csscld  25297  clsocv  25298  itg2gt0  25810  dvmptadd  26013  dvmptmul  26014  dvmptco  26025  logcn  26704  selberglem1  27604  noseq0  28311  hmopidmchi  32180  evl1deg2  33582  sigagensiga  34122  dya2iocbrsiga  34257  dya2icobrsiga  34258  logdivsqrle  34644  fnessref  36340  bj-snexg  37017  bj-unexg  37021  unirep  37701  indexdom  37721  dicfnN  41166  pwslnmlem0  43080  mendval  43168  icof  45162  dvsubf  45870  dvdivf  45878  itgsinexplem1  45910  stirlinglem7  46036  fourierdlem73  46135  fouriersw  46187  ovolval4lem1  46605  i0oii  48716  io1ii  48717