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  5211  unisn2  5213  class2set  5251  snexALT  5281  snex  5329  prex  5330  onun2i  6303  iotaex  6332  fvrn0  6695  f0cli  6861  funsneqopb  6911  fmptsng  6927  fmptsnd  6928  elimdelov  7247  ovima0  7324  ndmovcl  7330  caovmo  7382  soex  7623  zfrep6  7653  1st2ndb  7726  wfrlem17  7968  smofvon2  7990  tz7.44-2  8040  oesuclem  8147  omcl  8158  oecl  8159  nnmcl  8235  nnecl  8236  ixpexg  8483  resixpfo  8497  en1b  8574  xpsnen  8598  nnunifi  8766  xpfi  8786  fsuppun  8849  0fsupp  8852  oiexg  8996  hartogslem1  9003  cantnfvalf  9125  rankdmr1  9227  rankr1c  9247  numwdom  9482  alephon  9492  isfin5  9718  sdom2en01  9721  isf32lem9  9780  hsmexlem9  9844  iundom2g  9959  gchxpidm  10088  r1tskina  10201  tskmcl  10260  recmulnq  10383  recclnq  10385  genpelv  10419  un0mulcl  11929  znegcl  12015  zeo  12066  eqreznegel  12332  xnegcl  12604  xnn0xaddcl  12626  ioorebas  12837  modid0  13263  2txmodxeq0  13297  fzofi  13340  seqexw  13383  expcllem  13438  m1expcl2  13449  faclbnd4lem3  13653  bccl  13680  hasheq0  13722  hashrabrsn  13731  fnfz0hashnn0  13804  fnfzo0hashnn0  13807  wrdnfi  13895  ccat2s1p1OLD  13983  cshwcl  14156  relexpaddg  14408  abs00bd  14647  iserge0  15013  sumrblem  15064  fsumcvg  15065  summolem2a  15068  sumss  15077  fsumss  15078  fsumcvg2  15080  sumsplit  15119  binom  15181  bcxmas  15186  geomulcvg  15228  prodrblem  15279  fprodcvg  15280  prodmolem2a  15284  zprod  15287  fprodntriv  15292  prodss  15297  fprodss  15298  binomfallfac  15391  bpoly1  15401  bpoly2  15407  bpoly3  15408  ruclem6  15584  smupf  15823  gcdcl  15851  lcmcl  15941  lcmfcl  15968  2mulprm  16033  pcxcl  16193  pcmptcl  16223  infpnlem2  16243  zgz  16265  4sqlem2  16281  4sqlem19  16295  vdwapval  16305  hashbc0  16337  ramcl2  16348  0ramcl  16355  ramcl  16361  isstruct2  16489  imasval  16780  imasbas  16781  imasds  16782  imasplusg  16786  imasmulr  16787  imasvsca  16789  imasip  16790  imasle  16792  qusaddvallem  16820  qusaddflem  16821  qusaddval  16822  qusaddf  16823  qusmulval  16824  qusmulf  16825  mreexexlem3d  16913  sscpwex  17081  fullresc  17117  estrres  17385  evlfcl  17468  ipopos  17766  gsumress  17888  submnd0  17936  qusgrp2  18213  mulgfval  18222  issubg2  18290  triv1nsgd  18321  torsubg  18970  frgpnabllem1  18989  lt6abl  19011  ablfaclem3  19205  ablfac2  19207  simpgnsgd  19218  srgbinomlem3  19288  ringidss  19323  qusring2  19366  isdrngd  19523  mptscmfsupp0  19695  islss3  19727  lspsnel  19771  lspprel  19862  znf1o  20694  frgpcyg  20716  cnmsgnsubg  20717  phlpropd  20795  cssval  20822  iscss  20823  dsmm0cl  20880  uvcvvcl  20927  m1detdiag  21202  m2detleiblem1  21229  pmatcollpw3fi1lem1  21390  indistopon  21605  indiscld  21695  restbas  21762  ordttopon  21797  iocpnfordt  21819  icomnfordt  21820  lecldbas  21823  fiuncmp  22008  cmpfi  22012  conncompid  22035  dissnlocfin  22133  elpt  22176  xkotop  22192  xkouni  22203  xkohaus  22257  xkoptsub  22258  imastopn  22324  filconn  22487  cfinufil  22532  alexsublem  22648  alexsub  22649  alexsubALTlem4  22654  distgp  22703  indistgp  22704  ssblps  23028  ssbl  23029  xmeter  23039  nmoi  23333  nmoeq0  23341  0nghm  23346  idnghm  23348  icccld  23371  iocmnfcld  23373  blssioo  23399  xrtgioo  23410  xrsxmet  23413  icccmp  23429  pcopt  23622  pcopt2  23623  elpi1  23645  cmetcaulem  23887  ishl2  23969  rrxmvallem  24003  ovolcl  24075  ovolunlem1a  24093  ovolunnul  24097  ovoliunnul  24104  ioombl1  24159  icombl  24161  ioombl  24162  iccmbl  24163  iccvolcl  24164  ovolioo  24165  ioovolcl  24167  ioorcl  24174  uniioovol  24176  uniioombllem2a  24179  uniioombllem4  24183  uniioombllem5  24184  vitalilem1  24205  vitalilem5  24209  mbfconstlem  24224  mbfima  24227  mbfid  24232  ismbf2d  24237  mbfss  24243  mbfmulc2lem  24244  i1fd  24278  itg1addlem2  24294  itg1addlem4  24296  itg1addlem5  24297  i1fmulc  24300  itg2l  24326  itg2cl  24329  ibl0  24383  iblrelem  24387  iblpos  24389  iblss2  24402  bddmulibl  24435  bddiblnc  24438  recnperf  24501  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  31184  ordtrestNEW  31188  esumpad  31338  esumpad2  31339  esumcst  31346  esumrnmpt2  31351  sibf0  31616  sitgclcn  31626  sitgclre  31627  eulerpartlemgs2  31662  dstfrvclim1  31759  ballotlemfelz  31772  sgncl  31820  signstfveq0  31871  breprexp  31928  subfacp1lem3  32453  rellysconn  32522  cvmlift2lem9  32582  ordcmp  33819  finxpreclem4  34702  poimirlem16  34946  poimirlem17  34947  voliunnfl  34974  mbfresfi  34976  itg2addnclem2  34982  dvasin  35014  heiborlem4  35128  heiborlem6  35130  wepwsolem  39717  flcidc  39849  iocmbl  39894  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