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  7672  releldm2  7739  mapprc  8407  ixpprc  8480  bren  8515  brdomg  8516  domssex  8675  mapen  8678  ssenen  8688  fodomfib  8795  fi0  8881  dffi3  8892  brwdom  9028  brwdomn0  9030  unxpwdom2  9049  ixpiunwdom  9052  tcmin  9180  rankonid  9255  rankr1id  9288  cardf2  9369  cardid2  9379  carduni  9407  fseqen  9450  acndom  9474  acndom2  9477  alephnbtwn  9494  cardcf  9671  cfeq0  9675  cflim2  9682  coftr  9692  infpssr  9727  hsmexlem5  9849  axdc3lem4  9872  fodomb  9945  ondomon  9982  gruina  10237  ioof  12833  hashbc  13809  hashfacen  13810  trclun  14370  zsum  15071  fsum  15073  fprod  15291  eqgen  18329  symgfisg  18592  dvdsr  19392  asplss  20099  aspsubrg  20101  psrval  20138  clsf  21652  restco  21768  subbascn  21858  is2ndc  22050  ptbasin2  22182  ptbas  22183  indishmph  22402  ufldom  22566  cnextfres1  22672  ussid  22865  icopnfcld  23372  cnrehmeo  23553  csscld  23848  clsocv  23849  itg2gt0  24357  dvmptadd  24555  dvmptmul  24556  dvmptco  24567  logcn  25228  selberglem1  26119  hmopidmchi  29926  sigagensiga  31424  dya2iocbrsiga  31557  dya2icobrsiga  31558  logdivsqrle  31945  fnessref  33729  unirep  35024  indexdom  35045  dicfnN  38355  pwslnmlem0  39766  mendval  39858  icof  41556  dvsubf  42272  dvdivf  42281  itgsinexplem1  42313  stirlinglem7  42439  fourierdlem73  42538  fouriersw  42590  ovolval4lem1  43005