Theorem eqeltrrdi 2874

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  axrep6g  5253  snexgALT  5414  wemoiso2  7977  releldm2  8046  mapprc  8834  mapfoss  8855  ixpprc  8923  bren  8959  brdomg  8961  domssex  9133  mapen  9136  ssenen  9146  fodomfib  9295  fi0  9387  dffi3  9398  brwdom  9536  brwdomn0  9538  unxpwdom2  9557  ixpiunwdom  9559  tcmin  9715  rankonid  9808  rankr1id  9841  cardf2  9945  cardid2  9955  carduni  9983  fseqen  10027  acndom  10051  acndom2  10054  alephnbtwn  10071  cardcf  10250  cfeq0  10255  cflim2  10262  coftr  10272  infpssr  10307  hsmexlem5  10429  axdc3lem4  10452  fodomb  10525  ondomon  10564  gruina  10820  ioof  13492  hashbc  14510  trclun  15077  zsum  15794  fsum  15796  fprod  16020  eqgen  19295  symgfisg  19584  dvdsr  20492  asplss  22075  aspsubrg  22077  psrval  22117  clsf  23257  restco  23373  subbascn  23463  is2ndc  23655  ptbasin2  23788  ptbas  23789  indishmph  24008  ufldom  24172  cnextfres1  24278  ussid  24470  icopnfcld  24977  cnrehmeo  25165  csscld  25461  clsocv  25462  itg2gt0  25972  dvmptadd  26172  dvmptmul  26173  dvmptco  26184  logcn  26865  selberglem1  27762  noseq0  28536  hmopidmchi  32576  evl1deg2  33933  sigagensiga  34598  dya2iocbrsiga  34732  dya2icobrsiga  34733  logdivsqrle  35104  fnessref  36927  dfttc2g  37076  bj-snexg  37729  bj-unexg  37733  unirep  38425  indexdom  38445  dicfnN  42017  pwslnmlem0  43878  mendval  43966  orbitinit  45725  icof  45995  dvsubf  46688  dvdivf  46696  itgsinexplem1  46728  stirlinglem7  46854  fourierdlem73  46953  fouriersw  47005  ovolval4lem1  47423  lamberte  47685  i0oii  49757  io1ii  49758  2arwcatlem4  50435  2arwcat  50437