Theorem eqeltrdi 2920

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2813  df-clel 2892

This theorem is referenced by:  eqeltrrdi  2921  csbexg  5207  unisn2  5209  class2set  5247  snexALT  5277  snex  5325  prex  5326  onun2i  6299  iotaex  6328  fvrn0  6691  f0cli  6857  funsneqopb  6907  fmptsng  6923  fmptsnd  6924  elimdelov  7243  ovima0  7320  ndmovcl  7326  caovmo  7378  soex  7619  zfrep6  7649  1st2ndb  7722  wfrlem17  7964  smofvon2  7986  tz7.44-2  8036  oesuclem  8143  omcl  8154  oecl  8155  nnmcl  8231  nnecl  8232  ixpexg  8479  resixpfo  8493  en1b  8570  xpsnen  8594  nnunifi  8762  xpfi  8782  fsuppun  8845  0fsupp  8848  oiexg  8992  hartogslem1  8999  cantnfvalf  9121  rankdmr1  9223  rankr1c  9243  numwdom  9478  alephon  9488  isfin5  9714  sdom2en01  9717  isf32lem9  9776  hsmexlem9  9840  iundom2g  9955  gchxpidm  10084  r1tskina  10197  tskmcl  10256  recmulnq  10379  recclnq  10381  genpelv  10415  un0mulcl  11925  znegcl  12011  zeo  12062  eqreznegel  12328  xnegcl  12600  xnn0xaddcl  12622  ioorebas  12833  modid0  13262  2txmodxeq0  13296  fzofi  13339  seqexw  13382  expcllem  13437  m1expcl2  13448  faclbnd4lem3  13652  bccl  13679  hasheq0  13721  hashrabrsn  13730  fnfz0hashnn0  13803  fnfzo0hashnn0  13806  wrdnfi  13894  ccat2s1p1OLD  13982  cshwcl  14155  relexpaddg  14407  abs00bd  14646  iserge0  15012  sumrblem  15063  fsumcvg  15064  summolem2a  15067  sumss  15076  fsumss  15077  fsumcvg2  15079  sumsplit  15118  binom  15180  bcxmas  15185  geomulcvg  15227  prodrblem  15278  fprodcvg  15279  prodmolem2a  15283  zprod  15286  fprodntriv  15291  prodss  15296  fprodss  15297  binomfallfac  15390  bpoly1  15400  bpoly2  15406  bpoly3  15407  ruclem6  15583  smupf  15822  gcdcl  15850  lcmcl  15940  lcmfcl  15967  2mulprm  16032  pcxcl  16192  pcmptcl  16222  infpnlem2  16242  zgz  16264  4sqlem2  16280  4sqlem19  16294  vdwapval  16304  hashbc0  16336  ramcl2  16347  0ramcl  16354  ramcl  16360  isstruct2  16488  imasval  16779  imasbas  16780  imasds  16781  imasplusg  16785  imasmulr  16786  imasvsca  16788  imasip  16789  imasle  16791  qusaddvallem  16819  qusaddflem  16820  qusaddval  16821  qusaddf  16822  qusmulval  16823  qusmulf  16824  mreexexlem3d  16912  sscpwex  17080  fullresc  17116  estrres  17384  evlfcl  17467  ipopos  17765  gsumress  17887  submnd0  17935  qusgrp2  18212  mulgfval  18221  issubg2  18289  triv1nsgd  18320  torsubg  18969  frgpnabllem1  18988  lt6abl  19010  ablfaclem3  19204  ablfac2  19206  simpgnsgd  19217  srgbinomlem3  19287  ringidss  19322  qusring2  19365  isdrngd  19522  mptscmfsupp0  19694  islss3  19726  lspsnel  19770  lspprel  19861  znf1o  20693  frgpcyg  20715  cnmsgnsubg  20716  phlpropd  20794  cssval  20821  iscss  20822  dsmm0cl  20879  uvcvvcl  20926  m1detdiag  21201  m2detleiblem1  21228  pmatcollpw3fi1lem1  21389  indistopon  21604  indiscld  21694  restbas  21761  ordttopon  21796  iocpnfordt  21818  icomnfordt  21819  lecldbas  21822  fiuncmp  22007  cmpfi  22011  conncompid  22034  dissnlocfin  22132  elpt  22175  xkotop  22191  xkouni  22202  xkohaus  22256  xkoptsub  22257  imastopn  22323  filconn  22486  cfinufil  22531  alexsublem  22647  alexsub  22648  alexsubALTlem4  22653  distgp  22702  indistgp  22703  ssblps  23027  ssbl  23028  xmeter  23038  nmoi  23332  nmoeq0  23340  0nghm  23345  idnghm  23347  icccld  23370  iocmnfcld  23372  blssioo  23398  xrtgioo  23409  xrsxmet  23412  icccmp  23428  pcopt  23621  pcopt2  23622  elpi1  23644  cmetcaulem  23886  ishl2  23968  rrxmvallem  24002  ovolcl  24074  ovolunlem1a  24092  ovolunnul  24096  ovoliunnul  24103  ioombl1  24158  icombl  24160  ioombl  24161  iccmbl  24162  iccvolcl  24163  ovolioo  24164  ioovolcl  24166  ioorcl  24173  uniioovol  24175  uniioombllem2a  24178  uniioombllem4  24182  uniioombllem5  24183  vitalilem1  24204  vitalilem5  24208  mbfconstlem  24223  mbfima  24226  mbfid  24231  ismbf2d  24236  mbfss  24242  mbfmulc2lem  24243  i1fd  24277  itg1addlem2  24293  itg1addlem4  24295  itg1addlem5  24296  i1fmulc  24299  itg2l  24325  itg2cl  24328  ibl0  24382  iblrelem  24386  iblpos  24388  iblss2  24401  bddmulibl  24434  bddiblnc  24437  recnperf  24500  ply1remlem  24754  fta1glem1  24757  fta1g  24759  elply  24783  plypf1  24800  coefv0  24836  coemulc  24843  fta1  24895  elqaalem2  24907  aannenlem2  24916  aalioulem3  24921  taylfvallem1  24943  tayl0  24948  ulm0  24977  logtayl  25241  atanrecl  25487  atanbnd  25502  harmonicbnd3  25583  ftalem7  25654  basellem5  25660  ppifi  25681  sqff1o  25757  1sgmprm  25773  logexprlim  25799  dchrelbasd  25813  dchr1re  25837  lgslem4  25874  lgsne0  25909  2sqlem9  26001  2sqlem10  26002  rpvmasumlem  26061  dchrisumlem1  26063  vmalogdivsum  26113  pntrlog2bndlem5  26155  ostth  26213  tgcgr4  26315  axlowdimlem16  26741  fusgrfisbase  27108  vtxdg0e  27254  rgrusgrprc  27369  wwlksnfi  27682  clwwlknfiOLD  27822  trlsegvdeglem7  28003  eulerpathpr  28017  0blo  28567  nmlno0lem  28568  omlsilem  29177  pjoc1i  29206  nonbooli  29426  nmlnop0iALT  29770  unopbd  29790  leoprf2  29902  opsqrlem4  29918  opsqrlem5  29919  pjbdlni  29924  pjcmul1i  29976  prsssdm  31181  ordtrestNEW  31185  esumpad  31335  esumpad2  31336  esumcst  31343  esumrnmpt2  31348  sibf0  31613  sitgclcn  31623  sitgclre  31624  eulerpartlemgs2  31659  dstfrvclim1  31756  ballotlemfelz  31769  sgncl  31817  signstfveq0  31868  breprexp  31925  subfacp1lem3  32450  rellysconn  32519  cvmlift2lem9  32579  ordcmp  33816  finxpreclem4  34699  poimirlem16  34943  poimirlem17  34944  voliunnfl  34971  mbfresfi  34973  itg2addnclem2  34979  dvasin  35011  heiborlem4  35125  heiborlem6  35127  wepwsolem  39718  flcidc  39850  iocmbl  39895  arearect  39897  iscard4  39974  briunov2uz  40117  eliunov2uz  40118  frege124d  40180  frege129d  40182  frege92  40375  lhe4.4ex1a  40735  dvconstbi  40740  binomcxplemnn0  40755  binomcxplemnotnn0  40762  infxr  41709  infleinflem2  41713  climneg  41965  cncfiooicc  42251  itgsinexplem1  42313  volioof  42346  stoweidlem36  42395  wallispilem3  42426  fourierdlem93  42558  fouriersw  42590  fouriercn  42591  etransclem16  42609  etransclem33  42626  sge0reuz  42803  nnfoctbdjlem  42811  hoidmvlelem3  42953  dfatafv2ex  43486  sprsymrelfvlem  43726  fmtnofz04prm  43813  nnsum4primeseven  44039  nnsum4primesevenALTV  44040  lincext2  44584  blennn0elnn  44711