Theorem eqeltrdi 2837

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eqeltrrdi  2838  csbexg  5268  unisn2  5270  class2set  5313  snexALT  5341  snex  5394  prex  5395  iotaex  6487  iotaexOLD  6494  fvrn0  6891  f0cli  7073  funsneqopb  7127  fmptsng  7145  fmptsnd  7146  elimdelov  7488  ovima0  7571  ndmovcl  7577  caovmo  7629  soex  7900  zfrep6  7936  1st2ndb  8011  fprresex  8292  smofvon2  8328  tz7.44-2  8378  oesuclem  8492  omcl  8503  oecl  8504  nnmcl  8579  nnecl  8580  fsetex  8832  fsetexb  8840  ixpexg  8898  resixpfo  8912  xpsnen  9029  ssfi  9143  cnvfi  9146  nnunifi  9245  imafiOLD  9272  xpfiOLD  9277  prfi  9281  fsuppun  9345  0fsupp  9348  oiexg  9495  hartogslem1  9502  cantnfvalf  9625  rnttrcl  9682  ttrclse  9687  rankdmr1  9761  rankr1c  9781  numwdom  10019  alephon  10029  isfin5  10259  sdom2en01  10262  isf32lem9  10321  hsmexlem9  10385  iundom2g  10500  gchxpidm  10629  r1tskina  10742  tskmcl  10801  recmulnq  10924  recclnq  10926  genpelv  10960  un0mulcl  12483  znegcl  12575  zeo  12627  eqreznegel  12900  xnegcl  13180  xnn0xaddcl  13202  ioorebas  13419  modid0  13866  2txmodxeq0  13903  fzofi  13946  seqexw  13989  expcllem  14044  m1expcl2  14057  faclbnd4lem3  14267  bccl  14294  hasheq0  14335  hashrabrsn  14344  fnfz0hashnn0  14420  fnfzo0hashnn0  14423  wrdnfi  14520  cshwcl  14770  relexpaddg  15026  abs00bd  15264  iserge0  15634  sumrblem  15684  fsumcvg  15685  summolem2a  15688  sumss  15697  fsumss  15698  fsumcvg2  15700  sumsplit  15741  binom  15803  bcxmas  15808  geomulcvg  15849  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  fprodntriv  15915  prodss  15920  fprodss  15921  binomfallfac  16014  bpoly1  16024  bpoly2  16030  bpoly3  16031  ruclem6  16210  smupf  16455  gcdcl  16483  lcmcl  16578  lcmfcl  16605  2mulprm  16670  pcxnn0cl  16838  pcxcl  16839  pcmptcl  16869  infpnlem2  16889  zgz  16911  4sqlem2  16927  4sqlem19  16941  vdwapval  16951  hashbc0  16983  ramcl2  16994  0ramcl  17001  ramcl  17007  isstruct2  17126  imasval  17481  imasbas  17482  imasds  17483  imasplusg  17487  imasmulr  17488  imasvsca  17490  imasip  17491  imasle  17493  qusaddvallem  17521  qusaddflem  17522  qusaddval  17523  qusaddf  17524  qusmulval  17525  qusmulf  17526  mreexexlem3d  17614  sscpwex  17784  fullresc  17820  estrres  18107  evlfcl  18190  ipopos  18502  gsumress  18616  submnd0  18697  qusgrp2  18997  mulgfval  19008  issubg2  19080  triv1nsgd  19112  0subgALT  19505  torsubg  19791  frgpnabllem1  19810  lt6abl  19832  ablfaclem3  20026  ablfac2  20028  simpgnsgd  20039  qusrng  20096  srgbinomlem3  20144  ringidss  20193  qusring2  20250  isdrngd  20681  isdrngdOLD  20683  mptscmfsupp0  20840  islss3  20872  ellspsn  20916  lspprel  21008  znf1o  21468  frgpcyg  21490  cnmsgnsubg  21493  phlpropd  21571  cssval  21598  iscss  21599  dsmm0cl  21656  uvcvvcl  21703  m1detdiag  22491  m2detleiblem1  22518  pmatcollpw3fi1lem1  22680  indistopon  22895  indiscld  22985  restbas  23052  ordttopon  23087  iocpnfordt  23109  icomnfordt  23110  lecldbas  23113  fiuncmp  23298  cmpfi  23302  conncompid  23325  dissnlocfin  23423  elpt  23466  xkotop  23482  xkouni  23493  xkohaus  23547  xkoptsub  23548  imastopn  23614  filconn  23777  cfinufil  23822  alexsublem  23938  alexsub  23939  alexsubALTlem4  23944  distgp  23993  indistgp  23994  ssblps  24317  ssbl  24318  xmeter  24328  nmoi  24623  nmoeq0  24631  0nghm  24636  idnghm  24638  icccld  24661  iocmnfcld  24663  blssioo  24690  xrtgioo  24702  xrsxmet  24705  icccmp  24721  pcopt  24929  pcopt2  24930  elpi1  24952  cmetcaulem  25195  ishl2  25277  rrxmvallem  25311  ovolcl  25386  ovolunlem1a  25404  ovolunnul  25408  ovoliunnul  25415  ioombl1  25470  icombl  25472  ioombl  25473  iccmbl  25474  iccvolcl  25475  ovolioo  25476  ioovolcl  25478  ioorcl  25485  uniioovol  25487  uniioombllem2a  25490  uniioombllem4  25494  uniioombllem5  25495  vitalilem1  25516  vitalilem5  25520  mbfconstlem  25535  mbfima  25538  mbfid  25543  ismbf2d  25548  mbfss  25554  mbfmulc2lem  25555  i1fd  25589  itg1addlem2  25605  itg1addlem4  25607  itg1addlem5  25608  i1fmulc  25611  itg2l  25637  itg2cl  25640  ibl0  25695  iblrelem  25699  iblpos  25701  iblss2  25714  bddmulibl  25747  bddiblnc  25750  recnperf  25813  ply1remlem  26077  fta1glem1  26080  fta1g  26082  elply  26107  plypf1  26124  coefv0  26160  coemulc  26167  fta1  26223  elqaalem2  26235  aannenlem2  26244  aalioulem3  26249  taylfvallem1  26271  tayl0  26276  ulm0  26307  logtayl  26576  atanrecl  26828  atanbnd  26843  harmonicbnd3  26925  ftalem7  26996  basellem5  27002  ppifi  27023  sqff1o  27099  1sgmprm  27117  logexprlim  27143  dchrelbasd  27157  dchr1re  27181  lgslem4  27218  lgsne0  27253  2sqlem9  27345  2sqlem10  27346  rpvmasumlem  27405  dchrisumlem1  27407  vmalogdivsum  27457  pntrlog2bndlem5  27499  ostth  27557  lrrecse  27856  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  noseqex  28190  n0mulscl  28244  n0sfincut  28253  eln0s  28258  n0subs  28260  n0zs  28284  expscllem  28323  elzs12  28344  tgcgr4  28465  axlowdimlem16  28891  fusgrfisbase  29262  vtxdg0e  29409  rgrusgrprc  29524  wwlksnfi  29843  trlsegvdeglem7  30162  eulerpathpr  30176  0blo  30728  nmlno0lem  30729  omlsilem  31338  pjoc1i  31367  nonbooli  31587  nmlnop0iALT  31931  unopbd  31951  leoprf2  32063  opsqrlem4  32079  opsqrlem5  32080  pjbdlni  32085  pjcmul1i  32137  mptiffisupp  32623  sgncl  32763  drngidlhash  33412  evl1deg1  33552  ply1dg1rt  33555  ply1dg3rt0irred  33558  m1pmeq  33559  lvecendof1f1o  33636  fldext2rspun  33684  constrabscl  33775  zarcmplem  33878  prsssdm  33914  ordtrestNEW  33918  esumpad  34052  esumpad2  34053  esumcst  34060  esumrnmpt2  34065  sibf0  34332  sitgclcn  34342  sitgclre  34343  eulerpartlemgs2  34378  dstfrvclim1  34476  ballotlemfelz  34489  signstfveq0  34575  breprexp  34631  wevgblacfn  35103  subfacp1lem3  35176  rellysconn  35245  cvmlift2lem9  35305  nnuni  35721  ordcmp  36442  bj-snex  37030  finxpreclem4  37389  poimirlem16  37637  poimirlem17  37638  voliunnfl  37665  mbfresfi  37667  itg2addnclem2  37673  dvasin  37705  heiborlem4  37815  heiborlem6  37817  itrere  42313  sn-itrere  42483  sn-retire  42484  wepwsolem  43038  flcidc  43166  iocmbl  43209  arearect  43211  omcl3g  43330  iscard4  43529  briunov2uz  43694  eliunov2uz  43695  frege124d  43757  frege129d  43759  frege92  43951  lhe4.4ex1a  44325  dvconstbi  44330  binomcxplemnn0  44345  binomcxplemnotnn0  44352  infxr  45370  infleinflem2  45374  climneg  45615  cncfiooicc  45899  itgsinexplem1  45959  volioof  45992  stoweidlem36  46041  wallispilem3  46072  fourierdlem93  46204  fouriersw  46236  fouriercn  46237  etransclem16  46255  etransclem33  46272  sge0reuz  46452  nnfoctbdjlem  46460  hoidmvlelem3  46602  upwordnul  46885  dfatafv2ex  47218  sprsymrelfvlem  47495  fmtnofz04prm  47582  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  gpg3nbgrvtx0  48071  lincext2  48448  blennn0elnn  48570  itcovalsucov  48661  resccat  49067  funcf2lem2  49075  isnatd  49216  swapfelvv  49256  fucoelvv  49313  prcofelvv  49373  termco  49474  prstcprs  49553