Theorem eqeltrrdi 2878

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  axrep6g  5255  snexgALT  5413  wemoiso2  7971  releldm2  8040  mapprc  8828  mapfoss  8849  ixpprc  8917  bren  8953  brdomg  8955  domssex  9126  mapen  9129  ssenen  9139  fodomfib  9288  fi0  9380  dffi3  9391  brwdom  9529  brwdomn0  9531  unxpwdom2  9550  ixpiunwdom  9552  tcmin  9708  rankonid  9801  rankr1id  9834  cardf2  9929  cardid2  9939  carduni  9967  fseqen  10011  acndom  10035  acndom2  10038  alephnbtwn  10055  cardcf  10235  cfeq0  10240  cflim2  10247  coftr  10257  infpssr  10292  hsmexlem5  10414  axdc3lem4  10437  fodomb  10510  ondomon  10547  gruina  10803  ioof  13474  hashbc  14490  trclun  15051  zsum  15769  fsum  15771  fprod  15995  eqgen  19249  symgfisg  19538  dvdsr  20444  asplss  21992  aspsubrg  21994  psrval  22034  clsf  23174  restco  23290  subbascn  23380  is2ndc  23572  ptbasin2  23704  ptbas  23705  indishmph  23924  ufldom  24088  cnextfres1  24194  ussid  24386  icopnfcld  24893  cnrehmeo  25081  csscld  25377  clsocv  25378  itg2gt0  25888  dvmptadd  26088  dvmptmul  26089  dvmptco  26100  logcn  26778  selberglem1  27675  noseq0  28449  hmopidmchi  32444  evl1deg2  33812  sigagensiga  34476  dya2iocbrsiga  34610  dya2icobrsiga  34611  logdivsqrle  34982  fnessref  36757  dfttc2g  36906  bj-snexg  37558  bj-unexg  37562  unirep  38253  indexdom  38273  dicfnN  41847  pwslnmlem0  43710  mendval  43798  orbitinit  45557  icof  45827  dvsubf  46520  dvdivf  46528  itgsinexplem1  46560  stirlinglem7  46686  fourierdlem73  46785  fouriersw  46837  ovolval4lem1  47255  lamberte  47514  i0oii  49583  io1ii  49584  2arwcatlem4  50261  2arwcat  50263