Theorem eqeltrrdi 2843

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  axrep6g  5233  snexg  5378  wemoiso2  7916  releldm2  7985  mapprc  8765  mapfoss  8787  ixpprc  8855  bren  8891  brdomg  8893  domssex  9064  mapen  9067  ssenen  9077  imafiOLD  9214  fodomfib  9227  fodomfibOLD  9229  fi0  9321  dffi3  9332  brwdom  9470  brwdomn0  9472  unxpwdom2  9491  ixpiunwdom  9493  tcmin  9646  rankonid  9739  rankr1id  9772  cardf2  9853  cardid2  9863  carduni  9891  fseqen  9935  acndom  9959  acndom2  9962  alephnbtwn  9979  cardcf  10160  cfeq0  10164  cflim2  10171  coftr  10181  infpssr  10216  hsmexlem5  10338  axdc3lem4  10361  fodomb  10434  ondomon  10471  gruina  10727  ioof  13361  hashbc  14374  trclun  14935  zsum  15639  fsum  15641  fprod  15862  eqgen  19108  symgfisg  19395  dvdsr  20296  asplss  21827  aspsubrg  21829  psrval  21869  clsf  22990  restco  23106  subbascn  23196  is2ndc  23388  ptbasin2  23520  ptbas  23521  indishmph  23740  ufldom  23904  cnextfres1  24010  ussid  24202  icopnfcld  24709  cnrehmeo  24905  cnrehmeoOLD  24906  csscld  25203  clsocv  25204  itg2gt0  25715  dvmptadd  25918  dvmptmul  25919  dvmptco  25930  logcn  26610  selberglem1  27510  noseq0  28251  hmopidmchi  32175  evl1deg2  33607  sigagensiga  34247  dya2iocbrsiga  34381  dya2icobrsiga  34382  logdivsqrle  34756  fnessref  36500  bj-snexg  37178  bj-unexg  37182  unirep  37854  indexdom  37874  dicfnN  41382  pwslnmlem0  43275  mendval  43363  orbitinit  45139  icof  45405  dvsubf  46100  dvdivf  46108  itgsinexplem1  46140  stirlinglem7  46266  fourierdlem73  46365  fouriersw  46417  ovolval4lem1  46835  lamberte  47076  i0oii  49107  io1ii  49108  2arwcatlem4  49785  2arwcat  49787