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

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

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  axrep6g  5290  snexg  5435  wemoiso2  7999  releldm2  8068  mapprc  8870  mapfoss  8892  ixpprc  8959  bren  8995  brdomg  8997  brdomgOLD  8998  domssex  9178  mapen  9181  ssenen  9191  imafiOLD  9354  fodomfib  9369  fodomfibOLD  9371  fi0  9460  dffi3  9471  brwdom  9607  brwdomn0  9609  unxpwdom2  9628  ixpiunwdom  9630  tcmin  9781  rankonid  9869  rankr1id  9902  cardf2  9983  cardid2  9993  carduni  10021  fseqen  10067  acndom  10091  acndom2  10094  alephnbtwn  10111  cardcf  10292  cfeq0  10296  cflim2  10303  coftr  10313  infpssr  10348  hsmexlem5  10470  axdc3lem4  10493  fodomb  10566  ondomon  10603  gruina  10858  ioof  13487  hashbc  14492  trclun  15053  zsum  15754  fsum  15756  fprod  15977  eqgen  19199  symgfisg  19486  dvdsr  20362  asplss  21894  aspsubrg  21896  psrval  21935  clsf  23056  restco  23172  subbascn  23262  is2ndc  23454  ptbasin2  23586  ptbas  23587  indishmph  23806  ufldom  23970  cnextfres1  24076  ussid  24269  icopnfcld  24788  cnrehmeo  24984  cnrehmeoOLD  24985  csscld  25283  clsocv  25284  itg2gt0  25795  dvmptadd  25998  dvmptmul  25999  dvmptco  26010  logcn  26689  selberglem1  27589  noseq0  28296  hmopidmchi  32170  evl1deg2  33602  sigagensiga  34142  dya2iocbrsiga  34277  dya2icobrsiga  34278  logdivsqrle  34665  fnessref  36358  bj-snexg  37035  bj-unexg  37039  unirep  37721  indexdom  37741  dicfnN  41185  pwslnmlem0  43103  mendval  43191  icof  45224  dvsubf  45929  dvdivf  45937  itgsinexplem1  45969  stirlinglem7  46095  fourierdlem73  46194  fouriersw  46246  ovolval4lem1  46664  i0oii  48817  io1ii  48818