Theorem eqeltrrdi 2921

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2813  df-clel 2892

This theorem is referenced by:  wemoiso2  7668  releldm2  7735  mapprc  8403  ixpprc  8476  bren  8511  brdomg  8512  domssex  8671  mapen  8674  ssenen  8684  fodomfib  8791  fi0  8877  dffi3  8888  brwdom  9024  brwdomn0  9026  unxpwdom2  9045  ixpiunwdom  9048  tcmin  9176  rankonid  9251  rankr1id  9284  cardf2  9365  cardid2  9375  carduni  9403  fseqen  9446  acndom  9470  acndom2  9473  alephnbtwn  9490  cardcf  9667  cfeq0  9671  cflim2  9678  coftr  9688  infpssr  9723  hsmexlem5  9845  axdc3lem4  9868  fodomb  9941  ondomon  9978  gruina  10233  ioof  12829  hashbc  13808  hashfacen  13809  trclun  14369  zsum  15070  fsum  15072  fprod  15290  eqgen  18328  symgfisg  18591  dvdsr  19391  asplss  20098  aspsubrg  20100  psrval  20137  clsf  21651  restco  21767  subbascn  21857  is2ndc  22049  ptbasin2  22181  ptbas  22182  indishmph  22401  ufldom  22565  cnextfres1  22671  ussid  22864  icopnfcld  23371  cnrehmeo  23552  csscld  23847  clsocv  23848  itg2gt0  24356  dvmptadd  24554  dvmptmul  24555  dvmptco  24566  logcn  25228  selberglem1  26119  hmopidmchi  29926  sigagensiga  31421  dya2iocbrsiga  31554  dya2icobrsiga  31555  logdivsqrle  31942  fnessref  33726  unirep  35021  indexdom  35042  dicfnN  38352  pwslnmlem0  39767  mendval  39859  icof  41556  dvsubf  42272  dvdivf  42281  itgsinexplem1  42313  stirlinglem7  42439  fourierdlem73  42538  fouriersw  42590  ovolval4lem1  43005