Theorem eqeltrrdi 2872

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  axrep6g  5251  snexgALT  5412  wemoiso2  7967  releldm2  8036  mapprc  8824  mapfoss  8845  ixpprc  8913  bren  8949  brdomg  8951  domssex  9122  mapen  9125  ssenen  9135  fodomfib  9284  fi0  9376  dffi3  9387  brwdom  9525  brwdomn0  9527  unxpwdom2  9546  ixpiunwdom  9548  tcmin  9704  rankonid  9797  rankr1id  9830  cardf2  9925  cardid2  9935  carduni  9963  fseqen  10007  acndom  10031  acndom2  10034  alephnbtwn  10051  cardcf  10230  cfeq0  10235  cflim2  10242  coftr  10252  infpssr  10287  hsmexlem5  10409  axdc3lem4  10432  fodomb  10505  ondomon  10542  gruina  10798  ioof  13469  hashbc  14486  trclun  15047  zsum  15765  fsum  15767  fprod  15991  eqgen  19244  symgfisg  19533  dvdsr  20440  asplss  22023  aspsubrg  22025  psrval  22065  clsf  23205  restco  23321  subbascn  23411  is2ndc  23603  ptbasin2  23735  ptbas  23736  indishmph  23955  ufldom  24119  cnextfres1  24225  ussid  24417  icopnfcld  24924  cnrehmeo  25112  csscld  25408  clsocv  25409  itg2gt0  25919  dvmptadd  26119  dvmptmul  26120  dvmptco  26131  logcn  26812  selberglem1  27709  noseq0  28483  hmopidmchi  32503  evl1deg2  33867  sigagensiga  34531  dya2iocbrsiga  34665  dya2icobrsiga  34666  logdivsqrle  35037  fnessref  36888  dfttc2g  37037  bj-snexg  37690  bj-unexg  37694  unirep  38385  indexdom  38405  dicfnN  41977  pwslnmlem0  43838  mendval  43926  orbitinit  45685  icof  45955  dvsubf  46648  dvdivf  46656  itgsinexplem1  46688  stirlinglem7  46814  fourierdlem73  46913  fouriersw  46965  ovolval4lem1  47383  lamberte  47645  i0oii  49718  io1ii  49719  2arwcatlem4  50396  2arwcat  50398