Theorem eqeltrrdi 2850

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 2849	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2818

This theorem is referenced by:  wemoiso2  7810  releldm2  7877  mapprc  8602  mapfoss  8623  ixpprc  8690  bren  8726  brenOLD  8727  brdomg  8729  brdomgOLD  8730  domssex  8907  mapen  8910  ssenen  8920  imafi  8940  fodomfib  9071  fi0  9157  dffi3  9168  brwdom  9304  brwdomn0  9306  unxpwdom2  9325  ixpiunwdom  9327  tcmin  9499  rankonid  9588  rankr1id  9621  cardf2  9702  cardid2  9712  carduni  9740  fseqen  9784  acndom  9808  acndom2  9811  alephnbtwn  9828  cardcf  10009  cfeq0  10013  cflim2  10020  coftr  10030  infpssr  10065  hsmexlem5  10187  axdc3lem4  10210  fodomb  10283  ondomon  10320  gruina  10575  ioof  13178  hashbc  14163  hashfacenOLD  14165  trclun  14723  zsum  15428  fsum  15430  fprod  15649  eqgen  18807  symgfisg  19074  dvdsr  19886  asplss  21076  aspsubrg  21078  psrval  21116  clsf  22197  restco  22313  subbascn  22403  is2ndc  22595  ptbasin2  22727  ptbas  22728  indishmph  22947  ufldom  23111  cnextfres1  23217  ussid  23410  icopnfcld  23929  cnrehmeo  24114  csscld  24411  clsocv  24412  itg2gt0  24923  dvmptadd  25122  dvmptmul  25123  dvmptco  25134  logcn  25800  selberglem1  26691  hmopidmchi  30509  sigagensiga  32105  dya2iocbrsiga  32238  dya2icobrsiga  32239  logdivsqrle  32626  fnessref  34542  unirep  35867  indexdom  35888  dicfnN  39193  pwslnmlem0  40913  mendval  41005  icof  42729  dvsubf  43426  dvdivf  43434  itgsinexplem1  43466  stirlinglem7  43592  fourierdlem73  43691  fouriersw  43743  ovolval4lem1  44158  i0oii  46182  io1ii  46183