Theorem eqeltrrdi 2845

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

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

This theorem is referenced by:  axrep6g  5225  snexgALT  5383  wemoiso2  7927  releldm2  7996  mapprc  8777  mapfoss  8799  ixpprc  8867  bren  8903  brdomg  8905  domssex  9076  mapen  9079  ssenen  9089  imafiOLD  9226  fodomfib  9239  fodomfibOLD  9241  fi0  9333  dffi3  9344  brwdom  9482  brwdomn0  9484  unxpwdom2  9503  ixpiunwdom  9505  tcmin  9660  rankonid  9753  rankr1id  9786  cardf2  9867  cardid2  9877  carduni  9905  fseqen  9949  acndom  9973  acndom2  9976  alephnbtwn  9993  cardcf  10174  cfeq0  10178  cflim2  10185  coftr  10195  infpssr  10230  hsmexlem5  10352  axdc3lem4  10375  fodomb  10448  ondomon  10485  gruina  10741  ioof  13400  hashbc  14415  trclun  14976  zsum  15680  fsum  15682  fprod  15906  eqgen  19156  symgfisg  19443  dvdsr  20342  asplss  21853  aspsubrg  21855  psrval  21895  clsf  23013  restco  23129  subbascn  23219  is2ndc  23411  ptbasin2  23543  ptbas  23544  indishmph  23763  ufldom  23927  cnextfres1  24033  ussid  24225  icopnfcld  24732  cnrehmeo  24920  csscld  25216  clsocv  25217  itg2gt0  25727  dvmptadd  25927  dvmptmul  25928  dvmptco  25939  logcn  26611  selberglem1  27508  noseq0  28282  hmopidmchi  32222  evl1deg2  33637  sigagensiga  34285  dya2iocbrsiga  34419  dya2icobrsiga  34420  logdivsqrle  34794  fnessref  36539  dfttc2g  36688  bj-snexg  37341  bj-unexg  37345  unirep  38035  indexdom  38055  dicfnN  41629  pwslnmlem0  43519  mendval  43607  orbitinit  45383  icof  45648  dvsubf  46342  dvdivf  46350  itgsinexplem1  46382  stirlinglem7  46508  fourierdlem73  46607  fouriersw  46659  ovolval4lem1  47077  lamberte  47336  i0oii  49395  io1ii  49396  2arwcatlem4  50073  2arwcat  50075