Theorem eqeltrrdi 2853

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  axrep6g  5311  snexg  5450  wemoiso2  8015  releldm2  8084  mapprc  8888  mapfoss  8910  ixpprc  8977  bren  9013  brenOLD  9014  brdomg  9016  brdomgOLD  9017  domssex  9204  mapen  9207  ssenen  9217  imafiOLD  9382  fodomfib  9397  fodomfibOLD  9399  fi0  9489  dffi3  9500  brwdom  9636  brwdomn0  9638  unxpwdom2  9657  ixpiunwdom  9659  tcmin  9810  rankonid  9898  rankr1id  9931  cardf2  10012  cardid2  10022  carduni  10050  fseqen  10096  acndom  10120  acndom2  10123  alephnbtwn  10140  cardcf  10321  cfeq0  10325  cflim2  10332  coftr  10342  infpssr  10377  hsmexlem5  10499  axdc3lem4  10522  fodomb  10595  ondomon  10632  gruina  10887  ioof  13507  hashbc  14502  trclun  15063  zsum  15766  fsum  15768  fprod  15989  eqgen  19221  symgfisg  19510  dvdsr  20388  asplss  21917  aspsubrg  21919  psrval  21958  clsf  23077  restco  23193  subbascn  23283  is2ndc  23475  ptbasin2  23607  ptbas  23608  indishmph  23827  ufldom  23991  cnextfres1  24097  ussid  24290  icopnfcld  24809  cnrehmeo  25003  cnrehmeoOLD  25004  csscld  25302  clsocv  25303  itg2gt0  25815  dvmptadd  26018  dvmptmul  26019  dvmptco  26030  logcn  26707  selberglem1  27607  noseq0  28314  hmopidmchi  32183  evl1deg2  33567  sigagensiga  34105  dya2iocbrsiga  34240  dya2icobrsiga  34241  logdivsqrle  34627  fnessref  36323  bj-snexg  37000  bj-unexg  37004  unirep  37674  indexdom  37694  dicfnN  41140  pwslnmlem0  43048  mendval  43140  icof  45126  dvsubf  45835  dvdivf  45843  itgsinexplem1  45875  stirlinglem7  46001  fourierdlem73  46100  fouriersw  46152  ovolval4lem1  46570  i0oii  48599  io1ii  48600