Theorem eqeltrrdi 2848

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  axrep6g  5212  snexgALT  5370  wemoiso2  7916  releldm2  7985  mapprc  8767  mapfoss  8789  ixpprc  8857  bren  8893  brdomg  8895  domssex  9066  mapen  9069  ssenen  9079  imafiOLD  9216  fodomfib  9229  fodomfibOLD  9231  fi0  9323  dffi3  9334  brwdom  9472  brwdomn0  9474  unxpwdom2  9493  ixpiunwdom  9495  tcmin  9651  rankonid  9744  rankr1id  9777  cardf2  9858  cardid2  9868  carduni  9896  fseqen  9940  acndom  9964  acndom2  9967  alephnbtwn  9984  cardcf  10165  cfeq0  10169  cflim2  10176  coftr  10186  infpssr  10221  hsmexlem5  10343  axdc3lem4  10366  fodomb  10439  ondomon  10476  gruina  10732  ioof  13391  hashbc  14406  trclun  14967  zsum  15671  fsum  15673  fprod  15897  eqgen  19147  symgfisg  19434  dvdsr  20333  asplss  21848  aspsubrg  21850  psrval  21890  clsf  23031  restco  23147  subbascn  23237  is2ndc  23429  ptbasin2  23561  ptbas  23562  indishmph  23781  ufldom  23945  cnextfres1  24051  ussid  24243  icopnfcld  24750  cnrehmeo  24938  csscld  25234  clsocv  25235  itg2gt0  25745  dvmptadd  25945  dvmptmul  25946  dvmptco  25957  logcn  26629  selberglem1  27526  noseq0  28300  hmopidmchi  32240  evl1deg2  33660  sigagensiga  34325  dya2iocbrsiga  34459  dya2icobrsiga  34460  logdivsqrle  34834  fnessref  36585  dfttc2g  36734  bj-snexg  37387  bj-unexg  37391  unirep  38081  indexdom  38101  dicfnN  41675  pwslnmlem0  43536  mendval  43624  orbitinit  45400  icof  45664  dvsubf  46357  dvdivf  46365  itgsinexplem1  46397  stirlinglem7  46523  fourierdlem73  46622  fouriersw  46674  ovolval4lem1  47092  lamberte  47351  i0oii  49410  io1ii  49411  2arwcatlem4  50088  2arwcat  50090