Theorem eqeltrrdi 2846

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  axrep6g  5226  snexgALT  5379  wemoiso2  7921  releldm2  7990  mapprc  8771  mapfoss  8793  ixpprc  8861  bren  8897  brdomg  8899  domssex  9070  mapen  9073  ssenen  9083  imafiOLD  9220  fodomfib  9233  fodomfibOLD  9235  fi0  9327  dffi3  9338  brwdom  9476  brwdomn0  9478  unxpwdom2  9497  ixpiunwdom  9499  tcmin  9654  rankonid  9747  rankr1id  9780  cardf2  9861  cardid2  9871  carduni  9899  fseqen  9943  acndom  9967  acndom2  9970  alephnbtwn  9987  cardcf  10168  cfeq0  10172  cflim2  10179  coftr  10189  infpssr  10224  hsmexlem5  10346  axdc3lem4  10369  fodomb  10442  ondomon  10479  gruina  10735  ioof  13394  hashbc  14409  trclun  14970  zsum  15674  fsum  15676  fprod  15900  eqgen  19150  symgfisg  19437  dvdsr  20336  asplss  21866  aspsubrg  21868  psrval  21908  clsf  23026  restco  23142  subbascn  23232  is2ndc  23424  ptbasin2  23556  ptbas  23557  indishmph  23776  ufldom  23940  cnextfres1  24046  ussid  24238  icopnfcld  24745  cnrehmeo  24933  csscld  25229  clsocv  25230  itg2gt0  25740  dvmptadd  25940  dvmptmul  25941  dvmptco  25952  logcn  26627  selberglem1  27525  noseq0  28299  hmopidmchi  32240  evl1deg2  33655  sigagensiga  34304  dya2iocbrsiga  34438  dya2icobrsiga  34439  logdivsqrle  34813  fnessref  36558  dfttc2g  36707  bj-snexg  37360  bj-unexg  37364  unirep  38052  indexdom  38072  dicfnN  41646  pwslnmlem0  43540  mendval  43628  orbitinit  45404  icof  45669  dvsubf  46363  dvdivf  46371  itgsinexplem1  46403  stirlinglem7  46529  fourierdlem73  46628  fouriersw  46680  ovolval4lem1  47098  lamberte  47351  i0oii  49410  io1ii  49411  2arwcatlem4  50088  2arwcat  50090