Theorem eqeltrrdi 2843

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

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

This theorem is referenced by:  axrep6g  5260  snexg  5405  wemoiso2  7973  releldm2  8042  mapprc  8844  mapfoss  8866  ixpprc  8933  bren  8969  brdomg  8971  brdomgOLD  8972  domssex  9152  mapen  9155  ssenen  9165  imafiOLD  9326  fodomfib  9341  fodomfibOLD  9343  fi0  9432  dffi3  9443  brwdom  9581  brwdomn0  9583  unxpwdom2  9602  ixpiunwdom  9604  tcmin  9755  rankonid  9843  rankr1id  9876  cardf2  9957  cardid2  9967  carduni  9995  fseqen  10041  acndom  10065  acndom2  10068  alephnbtwn  10085  cardcf  10266  cfeq0  10270  cflim2  10277  coftr  10287  infpssr  10322  hsmexlem5  10444  axdc3lem4  10467  fodomb  10540  ondomon  10577  gruina  10832  ioof  13464  hashbc  14471  trclun  15033  zsum  15734  fsum  15736  fprod  15957  eqgen  19164  symgfisg  19449  dvdsr  20322  asplss  21834  aspsubrg  21836  psrval  21875  clsf  22986  restco  23102  subbascn  23192  is2ndc  23384  ptbasin2  23516  ptbas  23517  indishmph  23736  ufldom  23900  cnextfres1  24006  ussid  24199  icopnfcld  24706  cnrehmeo  24902  cnrehmeoOLD  24903  csscld  25201  clsocv  25202  itg2gt0  25713  dvmptadd  25916  dvmptmul  25917  dvmptco  25928  logcn  26608  selberglem1  27508  noseq0  28236  hmopidmchi  32132  evl1deg2  33590  sigagensiga  34172  dya2iocbrsiga  34307  dya2icobrsiga  34308  logdivsqrle  34682  fnessref  36375  bj-snexg  37052  bj-unexg  37056  unirep  37738  indexdom  37758  dicfnN  41202  pwslnmlem0  43115  mendval  43203  orbitinit  44981  icof  45243  dvsubf  45943  dvdivf  45951  itgsinexplem1  45983  stirlinglem7  46109  fourierdlem73  46208  fouriersw  46260  ovolval4lem1  46678  lamberte  46920  i0oii  48894  io1ii  48895  2arwcatlem4  49475  2arwcat  49477