Theorem eqeltrrdi 2837

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  axrep6g  5240  snexg  5385  wemoiso2  7932  releldm2  8001  mapprc  8780  mapfoss  8802  ixpprc  8869  bren  8905  brdomg  8907  domssex  9079  mapen  9082  ssenen  9092  imafiOLD  9241  fodomfib  9256  fodomfibOLD  9258  fi0  9347  dffi3  9358  brwdom  9496  brwdomn0  9498  unxpwdom2  9517  ixpiunwdom  9519  tcmin  9670  rankonid  9758  rankr1id  9791  cardf2  9872  cardid2  9882  carduni  9910  fseqen  9956  acndom  9980  acndom2  9983  alephnbtwn  10000  cardcf  10181  cfeq0  10185  cflim2  10192  coftr  10202  infpssr  10237  hsmexlem5  10359  axdc3lem4  10382  fodomb  10455  ondomon  10492  gruina  10747  ioof  13384  hashbc  14394  trclun  14956  zsum  15660  fsum  15662  fprod  15883  eqgen  19095  symgfisg  19382  dvdsr  20282  asplss  21816  aspsubrg  21818  psrval  21857  clsf  22968  restco  23084  subbascn  23174  is2ndc  23366  ptbasin2  23498  ptbas  23499  indishmph  23718  ufldom  23882  cnextfres1  23988  ussid  24181  icopnfcld  24688  cnrehmeo  24884  cnrehmeoOLD  24885  csscld  25182  clsocv  25183  itg2gt0  25694  dvmptadd  25897  dvmptmul  25898  dvmptco  25909  logcn  26589  selberglem1  27489  noseq0  28224  hmopidmchi  32130  evl1deg2  33539  sigagensiga  34124  dya2iocbrsiga  34259  dya2icobrsiga  34260  logdivsqrle  34634  fnessref  36338  bj-snexg  37015  bj-unexg  37019  unirep  37701  indexdom  37721  dicfnN  41170  pwslnmlem0  43073  mendval  43161  orbitinit  44939  icof  45206  dvsubf  45905  dvdivf  45913  itgsinexplem1  45945  stirlinglem7  46071  fourierdlem73  46170  fouriersw  46222  ovolval4lem1  46640  lamberte  46882  i0oii  48901  io1ii  48902  2arwcatlem4  49580  2arwcat  49582