Theorem eqeltrdi 2871

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eqeltrrdi  2872  csbexg  5273  unisn2  5275  class2set  5325  snexALT  5354  snexOLD  5413  prexOLD  5414  iotaex  6512  fvrn0  6909  f0cli  7093  funsneqopb  7149  fmptsng  7166  fmptsnd  7167  elimdelov  7506  ovima0  7589  ndmovcl  7595  caovmo  7647  soex  7914  zfrep6OLD  7948  1st2ndb  8022  fprresex  8303  smofvon2  8339  tz7.44-2  8390  oesuclem  8506  omcl  8517  oecl  8518  nnmcl  8594  nnecl  8595  fsetex  8849  fsetexb  8857  ixpexg  8916  resixpfo  8930  xpsnen  9045  ssfi  9153  cnvfi  9156  nnunifi  9247  prfi  9279  fsuppun  9343  0fsupp  9346  oiexg  9493  hartogslem1  9500  cantnfvalf  9630  rnttrcl  9687  ttrclse  9692  rankdmr1  9769  rankr1c  9789  numwdom  10039  alephon  10049  isfin5  10278  sdom2en01  10281  isf32lem9  10340  hsmexlem9  10404  iundom2g  10519  gchxpidm  10649  r1tskina  10762  tskmcl  10821  recmulnq  10944  recclnq  10946  genpelv  10980  un0mulcl  12533  znegcl  12624  zeo  12677  eqreznegel  12953  xnegcl  13234  xnn0xaddcl  13256  ioorebas  13473  modid0  13926  2txmodxeq0  13963  fzofi  14006  seqexw  14049  expcllem  14104  m1expcl2  14117  faclbnd4lem3  14327  bccl  14354  hasheq0  14395  hashrabrsn  14404  fnfz0hashnn0  14481  fnfzo0hashnn0  14484  wrdnfi  14581  cshwcl  14831  relexpaddg  15086  sgncl  15130  abs00bd  15338  iserge0  15708  sumrblem  15758  fsumcvg  15759  summolem2a  15762  sumss  15771  fsumss  15772  fsumcvg2  15774  sumsplit  15815  binom  15880  bcxmas  15885  geomulcvg  15926  prodrblem  15979  fprodcvg  15980  prodmolem2a  15984  zprod  15987  fprodntriv  15992  prodss  15997  fprodss  15998  binomfallfac  16090  bpoly1  16100  bpoly2  16106  bpoly3  16107  ruclem6  16286  smupf  16531  gcdcl  16559  lcmcl  16654  lcmfcl  16681  2mulprm  16746  pcxnn0cl  16915  pcxcl  16916  pcmptcl  16946  infpnlem2  16966  zgz  16988  4sqlem2  17004  4sqlem19  17018  vdwapval  17028  hashbc0  17060  ramcl2  17071  0ramcl  17078  ramcl  17084  isstruct2  17204  imasval  17560  imasbas  17561  imasds  17562  imasplusg  17566  imasmulr  17567  imasvsca  17569  imasip  17570  imasle  17572  qusaddvallem  17600  qusaddflem  17601  qusaddval  17602  qusaddf  17603  qusmulval  17604  qusmulf  17605  mreexexlem3d  17697  sscpwex  17867  fullresc  17903  estrres  18190  evlfcl  18273  ipopos  18587  gsumress  18735  submnd0  18816  qusgrp2  19119  mulgfval  19130  issubg2  19203  triv1nsgd  19234  0subgALT  19633  torsubg  19919  frgpnabllem1  19938  lt6abl  19960  ablfaclem3  20154  ablfac2  20156  simpgnsgd  20167  qusrng  20253  srgbinomlem3  20305  ringidss  20356  qusring2  20412  isdrngd  20868  isdrngdOLD  20870  mptscmfsupp0  21048  islss3  21080  ellspsn  21124  lspprel  21215  znf1o  21701  frgpcyg  21723  cnmsgnsubg  21727  phlpropd  21805  cssval  21832  iscss  21833  dsmm0cl  21890  uvcvvcl  21937  m1detdiag  22754  m2detleiblem1  22781  pmatcollpw3fi1lem1  22943  indistopon  23158  indiscld  23248  restbas  23315  ordttopon  23350  iocpnfordt  23372  icomnfordt  23373  lecldbas  23376  fiuncmp  23561  cmpfi  23565  conncompid  23588  dissnlocfin  23686  elpt  23729  xkotop  23745  xkouni  23756  xkohaus  23810  xkoptsub  23811  imastopn  23877  filconn  24040  cfinufil  24085  alexsublem  24201  alexsub  24202  alexsubALTlem4  24207  distgp  24256  indistgp  24257  ssblps  24579  ssbl  24580  xmeter  24590  nmoi  24885  nmoeq0  24893  0nghm  24898  idnghm  24900  icccld  24923  iocmnfcld  24925  blssioo  24952  xrtgioo  24964  xrsxmet  24967  icccmp  24983  pcopt  25181  pcopt2  25182  elpi1  25204  cmetcaulem  25447  ishl2  25529  rrxmvallem  25563  ovolcl  25637  ovolunlem1a  25655  ovolunnul  25659  ovoliunnul  25666  ioombl1  25721  icombl  25723  ioombl  25724  iccmbl  25725  iccvolcl  25726  ovolioo  25727  ioovolcl  25729  ioorcl  25736  uniioovol  25738  uniioombllem2a  25741  uniioombllem4  25745  uniioombllem5  25746  vitalilem1  25767  vitalilem5  25771  mbfconstlem  25786  mbfima  25789  mbfid  25794  ismbf2d  25799  mbfss  25805  mbfmulc2lem  25806  i1fd  25840  itg1addlem2  25856  itg1addlem4  25858  itg1addlem5  25859  i1fmulc  25862  itg2l  25888  itg2cl  25891  ibl0  25946  iblrelem  25950  iblpos  25952  iblss2  25965  bddmulibl  25998  bddiblnc  26001  recnperf  26064  ply1remlem  26322  fta1glem1  26325  fta1g  26327  elply  26352  plypf1  26369  coefv0  26405  coemulc  26412  fta1  26469  elqaalem2  26481  aannenlem2  26492  aalioulem3  26497  taylfvallem1  26520  tayl0  26525  ulm0  26554  logtayl  26825  atanrecl  27076  atanbnd  27091  harmonicbnd3  27172  ftalem7  27243  basellem5  27249  ppifi  27270  sqff1o  27346  1sgmprm  27363  logexprlim  27389  dchrelbasd  27403  dchr1re  27427  lgslem4  27464  lgsne0  27499  2sqlem9  27591  2sqlem10  27592  rpvmasumlem  27651  dchrisumlem1  27653  vmalogdivsum  27703  pntrlog2bndlem5  27745  ostth  27803  lrrecse  28135  sltmuls1  28340  sltmuls2  28341  mulsuniflem  28342  noseqex  28482  n0mulscl  28538  n0fincut  28548  eln0s  28554  n0subs  28556  n0zs  28582  expscllem  28623  elz12s  28665  tgcgr4  28800  axlowdimlem16  29307  fusgrfisbase  29678  vtxdg0e  29824  rgrusgrprc  29939  wwlksnfi  30255  trlsegvdeglem7  30577  eulerpathpr  30591  0blo  31144  nmlno0lem  31145  omlsilem  31754  pjoc1i  31783  nonbooli  32003  nmlnop0iALT  32347  unopbd  32367  leoprf2  32479  opsqrlem4  32495  opsqrlem5  32496  pjbdlni  32501  pjcmul1i  32553  mptiffisupp  33038  drngidlhash  33741  evl1deg1  33866  ply1dg1rt  33870  ply1dg3rt0irred  33874  m1pmeq  33875  mplmulmvr  33929  esplyfvaln  33964  vieta  33970  lvecendof1f1o  34023  fldext2rspun  34072  constrabscl  34168  zarcmplem  34271  prsssdm  34307  ordtrestNEW  34311  esumpad  34445  esumpad2  34446  esumcst  34453  esumrnmpt2  34458  sibf0  34724  sitgclcn  34734  sitgclre  34735  eulerpartlemgs2  34770  dstfrvclim1  34868  ballotlemfelz  34881  signstfveq0  34964  breprexp  35020  r1wf  35489  fineqvnttrclselem1  35534  wevgblacfn  35595  subfacp1lem3  35674  rellysconn  35743  cvmlift2lem9  35803  nnuni  36219  ordcmp  36958  bj-snex  37671  finxpreclem4  38040  poimirlem16  38287  poimirlem17  38288  voliunnfl  38315  mbfresfi  38317  itg2addnclem2  38323  dvasin  38355  heiborlem4  38465  heiborlem6  38467  25or6to4  42973  itrere  43079  sn-itrere  43262  sn-retire  43263  wepwsolem  43769  flcidc  43897  iocmbl  43940  arearect  43942  omcl3g  44061  iscard4  44259  briunov2uz  44424  eliunov2uz  44425  frege124d  44487  frege129d  44489  frege92  44681  lhe4.4ex1a  45039  dvconstbi  45044  binomcxplemnn0  45059  binomcxplemnotnn0  45066  infxr  46082  infleinflem2  46086  climneg  46326  cncfiooicc  46608  itgsinexplem1  46668  volioof  46701  stoweidlem36  46750  wallispilem3  46781  fourierdlem93  46913  fouriersw  46945  fouriercn  46946  etransclem16  46964  etransclem33  46981  sge0reuz  47161  nnfoctbdjlem  47169  hoidmvlelem3  47311  sqrtqaa  47606  sinnpoly  47628  dfatafv2ex  47950  sprsymrelfvlem  48239  fmtnofz04prm  48329  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  gpg3nbgrvtx0  48841  lincext2  49235  blennn0elnn  49357  itcovalsucov  49448  resccat  49852  funcf2lem2  49860  isnatd  50001  swapfelvv  50041  fucoelvv  50098  prcofelvv  50158  termco  50259  prstcprs  50338