Theorem eqeltrrdi 2846

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  axrep6g  5237  snexgALT  5387  wemoiso2  7928  releldm2  7997  mapprc  8779  mapfoss  8801  ixpprc  8869  bren  8905  brdomg  8907  domssex  9078  mapen  9081  ssenen  9091  imafiOLD  9228  fodomfib  9241  fodomfibOLD  9243  fi0  9335  dffi3  9346  brwdom  9484  brwdomn0  9486  unxpwdom2  9505  ixpiunwdom  9507  tcmin  9660  rankonid  9753  rankr1id  9786  cardf2  9867  cardid2  9877  carduni  9905  fseqen  9949  acndom  9973  acndom2  9976  alephnbtwn  9993  cardcf  10174  cfeq0  10178  cflim2  10185  coftr  10195  infpssr  10230  hsmexlem5  10352  axdc3lem4  10375  fodomb  10448  ondomon  10485  gruina  10741  ioof  13375  hashbc  14388  trclun  14949  zsum  15653  fsum  15655  fprod  15876  eqgen  19125  symgfisg  19412  dvdsr  20313  asplss  21844  aspsubrg  21846  psrval  21886  clsf  23007  restco  23123  subbascn  23213  is2ndc  23405  ptbasin2  23537  ptbas  23538  indishmph  23757  ufldom  23921  cnextfres1  24027  ussid  24219  icopnfcld  24726  cnrehmeo  24922  cnrehmeoOLD  24923  csscld  25220  clsocv  25221  itg2gt0  25732  dvmptadd  25935  dvmptmul  25936  dvmptco  25947  logcn  26627  selberglem1  27527  noseq0  28301  hmopidmchi  32243  evl1deg2  33674  sigagensiga  34323  dya2iocbrsiga  34457  dya2icobrsiga  34458  logdivsqrle  34832  fnessref  36577  bj-snexg  37286  bj-unexg  37290  unirep  37969  indexdom  37989  dicfnN  41563  pwslnmlem0  43452  mendval  43540  orbitinit  45316  icof  45581  dvsubf  46276  dvdivf  46284  itgsinexplem1  46316  stirlinglem7  46442  fourierdlem73  46541  fouriersw  46593  ovolval4lem1  47011  lamberte  47252  i0oii  49283  io1ii  49284  2arwcatlem4  49961  2arwcat  49963