Theorem eqeltrrdi 2872

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 2871	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

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

This theorem is used by:  axrep6g  5245  snexgALT  5402  wemoiso2  7993  releldm2  8061  mapprc  8862  mapfoss  8885  ixpprc  8958  bren  8994  brdomg  8996  domssex  9168  mapen  9171  ssenen  9181  fodomfib  9331  fi0  9422  dffi3  9433  brwdom  9571  brwdomn0  9573  unxpwdom2  9592  ixpiunwdom  9594  tcmin  9750  rankonid  9849  rankr1id  9888  cardf2  10034  cardid2  10044  carduni  10072  fseqen  10116  acndom  10140  acndom2  10143  alephnbtwn  10160  cardcf  10339  cfeq0  10344  cflim2  10351  coftr  10361  infpssr  10396  hsmexlem5  10518  axdc3lem4  10541  fodomb  10615  ondomon  10657  gruina  10913  ioof  13588  hashbc  14608  trclun  15179  zsum  15896  fsum  15898  fprod  16120  eqgen  19405  symgfisg  19694  dvdsr  20604  asplss  22193  aspsubrg  22195  psrval  22235  clsf  23378  restco  23494  subbascn  23584  is2ndc  23776  ptbasin2  23909  ptbas  23910  indishmph  24129  ufldom  24293  cnextfres1  24399  ussid  24591  icopnfcld  25098  cnrehmeo  25286  csscld  25582  clsocv  25583  itg2gt0  26093  dvmptadd  26292  dvmptmul  26293  dvmptco  26304  logcn  26987  selberglem1  27884  noseq0  28688  hmopidmchi  32765  evl1deg2  34162  sigagensiga  34827  dya2iocbrsiga  34960  dya2icobrsiga  34961  logdivsqrle  35332  fnessref  37272  dfttc2g  37421  bj-snexg  38074  bj-unexg  38078  unirep  38788  indexdom  38808  dicfnN  42380  pwslnmlem0  44233  mendval  44321  orbitinit  46085  icof  46371  dvsubf  47063  dvdivf  47071  itgsinexplem1  47103  stirlinglem7  47229  fourierdlem73  47328  fouriersw  47380  ovolval4lem1  47798  lamberte  48077  i0oii  50173  io1ii  50174  2arwcatlem4  50875  2arwcat  50877