Theorem eqeltrdi 2844

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrdi.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrdi.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrdi

Step	Hyp	Ref	Expression
1		eqeltrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeltrdi.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2836	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 2708

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

This theorem is referenced by:  eqeltrrdi  2845  csbexg  5245  unisn2  5247  class2set  5296  snexALT  5325  snexOLD  5384  prexOLD  5385  iotaex  6474  fvrn0  6868  f0cli  7050  funsneqopb  7106  fmptsng  7123  fmptsnd  7124  elimdelov  7463  ovima0  7546  ndmovcl  7552  caovmo  7604  soex  7872  zfrep6OLD  7908  1st2ndb  7982  fprresex  8260  smofvon2  8296  tz7.44-2  8346  oesuclem  8460  omcl  8471  oecl  8472  nnmcl  8548  nnecl  8549  fsetex  8803  fsetexb  8811  ixpexg  8870  resixpfo  8884  xpsnen  8999  ssfi  9107  cnvfi  9110  nnunifi  9201  imafiOLD  9226  prfi  9234  fsuppun  9300  0fsupp  9303  oiexg  9450  hartogslem1  9457  cantnfvalf  9586  rnttrcl  9643  ttrclse  9648  rankdmr1  9725  rankr1c  9745  numwdom  9981  alephon  9991  isfin5  10221  sdom2en01  10224  isf32lem9  10283  hsmexlem9  10347  iundom2g  10462  gchxpidm  10592  r1tskina  10705  tskmcl  10764  recmulnq  10887  recclnq  10889  genpelv  10923  un0mulcl  12471  znegcl  12562  zeo  12615  eqreznegel  12884  xnegcl  13165  xnn0xaddcl  13187  ioorebas  13404  modid0  13856  2txmodxeq0  13893  fzofi  13936  seqexw  13979  expcllem  14034  m1expcl2  14047  faclbnd4lem3  14257  bccl  14284  hasheq0  14325  hashrabrsn  14334  fnfz0hashnn0  14410  fnfzo0hashnn0  14413  wrdnfi  14510  cshwcl  14760  relexpaddg  15015  abs00bd  15253  iserge0  15623  sumrblem  15673  fsumcvg  15674  summolem2a  15677  sumss  15686  fsumss  15687  fsumcvg2  15689  sumsplit  15730  binom  15795  bcxmas  15800  geomulcvg  15841  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  zprod  15902  fprodntriv  15907  prodss  15912  fprodss  15913  binomfallfac  16006  bpoly1  16016  bpoly2  16022  bpoly3  16023  ruclem6  16202  smupf  16447  gcdcl  16475  lcmcl  16570  lcmfcl  16597  2mulprm  16662  pcxnn0cl  16831  pcxcl  16832  pcmptcl  16862  infpnlem2  16882  zgz  16904  4sqlem2  16920  4sqlem19  16934  vdwapval  16944  hashbc0  16976  ramcl2  16987  0ramcl  16994  ramcl  17000  isstruct2  17119  imasval  17475  imasbas  17476  imasds  17477  imasplusg  17481  imasmulr  17482  imasvsca  17484  imasip  17485  imasle  17487  qusaddvallem  17515  qusaddflem  17516  qusaddval  17517  qusaddf  17518  qusmulval  17519  qusmulf  17520  mreexexlem3d  17612  sscpwex  17782  fullresc  17818  estrres  18105  evlfcl  18188  ipopos  18502  gsumress  18650  submnd0  18731  qusgrp2  19034  mulgfval  19045  issubg2  19117  triv1nsgd  19148  0subgALT  19543  torsubg  19829  frgpnabllem1  19848  lt6abl  19870  ablfaclem3  20064  ablfac2  20066  simpgnsgd  20077  qusrng  20161  srgbinomlem3  20209  ringidss  20258  qusring2  20314  isdrngd  20742  isdrngdOLD  20744  mptscmfsupp0  20922  islss3  20954  ellspsn  20998  lspprel  21089  znf1o  21531  frgpcyg  21553  cnmsgnsubg  21557  phlpropd  21635  cssval  21662  iscss  21663  dsmm0cl  21720  uvcvvcl  21767  m1detdiag  22562  m2detleiblem1  22589  pmatcollpw3fi1lem1  22751  indistopon  22966  indiscld  23056  restbas  23123  ordttopon  23158  iocpnfordt  23180  icomnfordt  23181  lecldbas  23184  fiuncmp  23369  cmpfi  23373  conncompid  23396  dissnlocfin  23494  elpt  23537  xkotop  23553  xkouni  23564  xkohaus  23618  xkoptsub  23619  imastopn  23685  filconn  23848  cfinufil  23893  alexsublem  24009  alexsub  24010  alexsubALTlem4  24015  distgp  24064  indistgp  24065  ssblps  24387  ssbl  24388  xmeter  24398  nmoi  24693  nmoeq0  24701  0nghm  24706  idnghm  24708  icccld  24731  iocmnfcld  24733  blssioo  24760  xrtgioo  24772  xrsxmet  24775  icccmp  24791  pcopt  24989  pcopt2  24990  elpi1  25012  cmetcaulem  25255  ishl2  25337  rrxmvallem  25371  ovolcl  25445  ovolunlem1a  25463  ovolunnul  25467  ovoliunnul  25474  ioombl1  25529  icombl  25531  ioombl  25532  iccmbl  25533  iccvolcl  25534  ovolioo  25535  ioovolcl  25537  ioorcl  25544  uniioovol  25546  uniioombllem2a  25549  uniioombllem4  25553  uniioombllem5  25554  vitalilem1  25575  vitalilem5  25579  mbfconstlem  25594  mbfima  25597  mbfid  25602  ismbf2d  25607  mbfss  25613  mbfmulc2lem  25614  i1fd  25648  itg1addlem2  25664  itg1addlem4  25666  itg1addlem5  25667  i1fmulc  25670  itg2l  25696  itg2cl  25699  ibl0  25754  iblrelem  25758  iblpos  25760  iblss2  25773  bddmulibl  25806  bddiblnc  25809  recnperf  25872  ply1remlem  26130  fta1glem1  26133  fta1g  26135  elply  26160  plypf1  26177  coefv0  26213  coemulc  26220  fta1  26274  elqaalem2  26286  aannenlem2  26295  aalioulem3  26300  taylfvallem1  26322  tayl0  26327  ulm0  26356  logtayl  26624  atanrecl  26875  atanbnd  26890  harmonicbnd3  26971  ftalem7  27042  basellem5  27048  ppifi  27069  sqff1o  27145  1sgmprm  27162  logexprlim  27188  dchrelbasd  27202  dchr1re  27226  lgslem4  27263  lgsne0  27298  2sqlem9  27390  2sqlem10  27391  rpvmasumlem  27450  dchrisumlem1  27452  vmalogdivsum  27502  pntrlog2bndlem5  27544  ostth  27602  lrrecse  27934  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  noseqex  28281  n0mulscl  28337  n0fincut  28347  eln0s  28353  n0subs  28355  n0zs  28381  expscllem  28422  elz12s  28464  tgcgr4  28599  axlowdimlem16  29026  fusgrfisbase  29397  vtxdg0e  29543  rgrusgrprc  29658  wwlksnfi  29974  trlsegvdeglem7  30296  eulerpathpr  30310  0blo  30863  nmlno0lem  30864  omlsilem  31473  pjoc1i  31502  nonbooli  31722  nmlnop0iALT  32066  unopbd  32086  leoprf2  32198  opsqrlem4  32214  opsqrlem5  32215  pjbdlni  32220  pjcmul1i  32272  mptiffisupp  32766  sgncl  32904  drngidlhash  33494  evl1deg1  33636  ply1dg1rt  33640  ply1dg3rt0irred  33644  m1pmeq  33645  mplmulmvr  33683  esplyfvaln  33718  vieta  33724  lvecendof1f1o  33777  fldext2rspun  33826  constrabscl  33922  zarcmplem  34025  prsssdm  34061  ordtrestNEW  34065  esumpad  34199  esumpad2  34200  esumcst  34207  esumrnmpt2  34212  sibf0  34478  sitgclcn  34488  sitgclre  34489  eulerpartlemgs2  34524  dstfrvclim1  34622  ballotlemfelz  34635  signstfveq0  34721  breprexp  34777  r1wf  35239  fineqvnttrclselem1  35265  wevgblacfn  35291  subfacp1lem3  35364  rellysconn  35433  cvmlift2lem9  35493  nnuni  35909  ordcmp  36629  bj-snex  37342  finxpreclem4  37710  poimirlem16  37957  poimirlem17  37958  voliunnfl  37985  mbfresfi  37987  itg2addnclem2  37993  dvasin  38025  heiborlem4  38135  heiborlem6  38137  itrere  42750  sn-itrere  42933  sn-retire  42934  wepwsolem  43470  flcidc  43598  iocmbl  43641  arearect  43643  omcl3g  43762  iscard4  43960  briunov2uz  44125  eliunov2uz  44126  frege124d  44188  frege129d  44190  frege92  44382  lhe4.4ex1a  44756  dvconstbi  44761  binomcxplemnn0  44776  binomcxplemnotnn0  44783  infxr  45796  infleinflem2  45800  climneg  46040  cncfiooicc  46322  itgsinexplem1  46382  volioof  46415  stoweidlem36  46464  wallispilem3  46495  fourierdlem93  46627  fouriersw  46659  fouriercn  46660  etransclem16  46678  etransclem33  46695  sge0reuz  46875  nnfoctbdjlem  46883  hoidmvlelem3  47025  sinnpoly  47339  dfatafv2ex  47661  sprsymrelfvlem  47950  fmtnofz04prm  48040  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  gpg3nbgrvtx0  48552  lincext2  48931  blennn0elnn  49053  itcovalsucov  49144  resccat  49549  funcf2lem2  49557  isnatd  49698  swapfelvv  49738  fucoelvv  49795  prcofelvv  49855  termco  49956  prstcprs  50035