Theorem eqeltrrdi 2873

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  axrep6g  5249  snexgALT  5406  wemoiso2  8020  releldm2  8088  mapprc  8889  mapfoss  8912  ixpprc  8985  bren  9021  brdomg  9023  domssex  9195  mapen  9198  ssenen  9208  fodomfib  9358  fi0  9449  dffi3  9460  brwdom  9598  brwdomn0  9600  unxpwdom2  9619  ixpiunwdom  9621  tcmin  9777  rankonid  9876  rankr1id  9915  cardf2  10061  cardid2  10071  carduni  10101  fseqen  10145  acndom  10169  acndom2  10172  alephnbtwn  10189  cardcf  10368  cfeq0  10373  cflim2  10380  coftr  10390  infpssr  10425  hsmexlem5  10547  axdc3lem4  10570  fodomb  10644  ondomon  10686  gruina  10942  ioof  13618  hashbc  14639  trclun  15210  zsum  15928  fsum  15930  fprod  16152  eqgen  19443  symgfisg  19733  dvdsr  20643  asplss  22236  aspsubrg  22238  psrval  22278  clsf  23421  restco  23537  subbascn  23627  is2ndc  23819  ptbasin2  23952  ptbas  23953  indishmph  24172  ufldom  24336  cnextfres1  24442  ussid  24634  icopnfcld  25141  cnrehmeo  25329  csscld  25625  clsocv  25626  itg2gt0  26136  dvmptadd  26335  dvmptmul  26336  dvmptco  26347  logcn  27032  selberglem1  27929  noseq0  28733  hmopidmchi  32810  evl1deg2  34212  sigagensiga  34885  dya2iocbrsiga  35018  dya2icobrsiga  35019  logdivsqrle  35390  fnessref  37360  dfttc2g  37509  bj-snexg  38162  bj-unexg  38166  unirep  38916  indexdom  38936  dicfnN  42506  pwslnmlem0  44359  mendval  44442  orbitinit  46210  icof  46505  dvsubf  47197  dvdivf  47205  itgsinexplem1  47237  stirlinglem7  47363  fourierdlem73  47462  fouriersw  47514  ovolval4lem1  47932  lamberte  48211  i0oii  50365  io1ii  50366  2arwcatlem4  51067  2arwcat  51069