Theorem eqeltrdi 2898

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eqeltrrdi  2899  csbexg  5178  unisn2  5180  class2set  5219  snexALT  5249  snex  5297  prex  5298  onun2i  6274  iotaex  6304  fvrn0  6673  f0cli  6841  funsneqopb  6891  fmptsng  6907  fmptsnd  6908  elimdelov  7229  ovima0  7307  ndmovcl  7313  caovmo  7365  soex  7608  zfrep6  7638  1st2ndb  7711  wfrlem17  7954  smofvon2  7976  tz7.44-2  8026  oesuclem  8133  omcl  8144  oecl  8145  nnmcl  8221  nnecl  8222  ixpexg  8469  resixpfo  8483  en1b  8560  xpsnen  8584  nnunifi  8753  xpfi  8773  fsuppun  8836  0fsupp  8839  oiexg  8983  hartogslem1  8990  cantnfvalf  9112  rankdmr1  9214  rankr1c  9234  numwdom  9470  alephon  9480  isfin5  9710  sdom2en01  9713  isf32lem9  9772  hsmexlem9  9836  iundom2g  9951  gchxpidm  10080  r1tskina  10193  tskmcl  10252  recmulnq  10375  recclnq  10377  genpelv  10411  un0mulcl  11919  znegcl  12005  zeo  12056  eqreznegel  12322  xnegcl  12594  xnn0xaddcl  12616  ioorebas  12829  modid0  13260  2txmodxeq0  13294  fzofi  13337  seqexw  13380  expcllem  13436  m1expcl2  13447  faclbnd4lem3  13651  bccl  13678  hasheq0  13720  hashrabrsn  13729  fnfz0hashnn0  13802  fnfzo0hashnn0  13805  wrdnfi  13891  ccat2s1p1OLD  13978  cshwcl  14151  relexpaddg  14404  abs00bd  14643  iserge0  15009  sumrblem  15060  fsumcvg  15061  summolem2a  15064  sumss  15073  fsumss  15074  fsumcvg2  15076  sumsplit  15115  binom  15177  bcxmas  15182  geomulcvg  15224  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprodntriv  15288  prodss  15293  fprodss  15294  binomfallfac  15387  bpoly1  15397  bpoly2  15403  bpoly3  15404  ruclem6  15580  smupf  15817  gcdcl  15845  lcmcl  15935  lcmfcl  15962  2mulprm  16027  pcxcl  16187  pcmptcl  16217  infpnlem2  16237  zgz  16259  4sqlem2  16275  4sqlem19  16289  vdwapval  16299  hashbc0  16331  ramcl2  16342  0ramcl  16349  ramcl  16355  isstruct2  16485  imasval  16776  imasbas  16777  imasds  16778  imasplusg  16782  imasmulr  16783  imasvsca  16785  imasip  16786  imasle  16788  qusaddvallem  16816  qusaddflem  16817  qusaddval  16818  qusaddf  16819  qusmulval  16820  qusmulf  16821  mreexexlem3d  16909  sscpwex  17077  fullresc  17113  estrres  17381  evlfcl  17464  ipopos  17762  gsumress  17884  submnd0  17932  qusgrp2  18209  mulgfval  18218  issubg2  18286  triv1nsgd  18317  torsubg  18967  frgpnabllem1  18986  lt6abl  19008  ablfaclem3  19202  ablfac2  19204  simpgnsgd  19215  srgbinomlem3  19285  ringidss  19323  qusring2  19366  isdrngd  19520  mptscmfsupp0  19692  islss3  19724  lspsnel  19768  lspprel  19859  znf1o  20243  frgpcyg  20265  cnmsgnsubg  20266  phlpropd  20344  cssval  20371  iscss  20372  dsmm0cl  20429  uvcvvcl  20476  m1detdiag  21202  m2detleiblem1  21229  pmatcollpw3fi1lem1  21391  indistopon  21606  indiscld  21696  restbas  21763  ordttopon  21798  iocpnfordt  21820  icomnfordt  21821  lecldbas  21824  fiuncmp  22009  cmpfi  22013  conncompid  22036  dissnlocfin  22134  elpt  22177  xkotop  22193  xkouni  22204  xkohaus  22258  xkoptsub  22259  imastopn  22325  filconn  22488  cfinufil  22533  alexsublem  22649  alexsub  22650  alexsubALTlem4  22655  distgp  22704  indistgp  22705  ssblps  23029  ssbl  23030  xmeter  23040  nmoi  23334  nmoeq0  23342  0nghm  23347  idnghm  23349  icccld  23372  iocmnfcld  23374  blssioo  23400  xrtgioo  23411  xrsxmet  23414  icccmp  23430  pcopt  23627  pcopt2  23628  elpi1  23650  cmetcaulem  23892  ishl2  23974  rrxmvallem  24008  ovolcl  24082  ovolunlem1a  24100  ovolunnul  24104  ovoliunnul  24111  ioombl1  24166  icombl  24168  ioombl  24169  iccmbl  24170  iccvolcl  24171  ovolioo  24172  ioovolcl  24174  ioorcl  24181  uniioovol  24183  uniioombllem2a  24186  uniioombllem4  24190  uniioombllem5  24191  vitalilem1  24212  vitalilem5  24216  mbfconstlem  24231  mbfima  24234  mbfid  24239  ismbf2d  24244  mbfss  24250  mbfmulc2lem  24251  i1fd  24285  itg1addlem2  24301  itg1addlem4  24303  itg1addlem5  24304  i1fmulc  24307  itg2l  24333  itg2cl  24336  ibl0  24390  iblrelem  24394  iblpos  24396  iblss2  24409  bddmulibl  24442  bddiblnc  24445  recnperf  24508  ply1remlem  24763  fta1glem1  24766  fta1g  24768  elply  24792  plypf1  24809  coefv0  24845  coemulc  24852  fta1  24904  elqaalem2  24916  aannenlem2  24925  aalioulem3  24930  taylfvallem1  24952  tayl0  24957  ulm0  24986  logtayl  25251  atanrecl  25497  atanbnd  25512  harmonicbnd3  25593  ftalem7  25664  basellem5  25670  ppifi  25691  sqff1o  25767  1sgmprm  25783  logexprlim  25809  dchrelbasd  25823  dchr1re  25847  lgslem4  25884  lgsne0  25919  2sqlem9  26011  2sqlem10  26012  rpvmasumlem  26071  dchrisumlem1  26073  vmalogdivsum  26123  pntrlog2bndlem5  26165  ostth  26223  tgcgr4  26325  axlowdimlem16  26751  fusgrfisbase  27118  vtxdg0e  27264  rgrusgrprc  27379  wwlksnfi  27692  trlsegvdeglem7  28011  eulerpathpr  28025  0blo  28575  nmlno0lem  28576  omlsilem  29185  pjoc1i  29214  nonbooli  29434  nmlnop0iALT  29778  unopbd  29798  leoprf2  29910  opsqrlem4  29926  opsqrlem5  29927  pjbdlni  29932  pjcmul1i  29984  zarcmplem  31234  prsssdm  31270  ordtrestNEW  31274  esumpad  31424  esumpad2  31425  esumcst  31432  esumrnmpt2  31437  sibf0  31702  sitgclcn  31712  sitgclre  31713  eulerpartlemgs2  31748  dstfrvclim1  31845  ballotlemfelz  31858  sgncl  31906  signstfveq0  31957  breprexp  32014  subfacp1lem3  32542  rellysconn  32611  cvmlift2lem9  32671  ordcmp  33908  finxpreclem4  34811  poimirlem16  35073  poimirlem17  35074  voliunnfl  35101  mbfresfi  35103  itg2addnclem2  35109  dvasin  35141  heiborlem4  35252  heiborlem6  35254  itrere  39591  retire  39592  wepwsolem  39986  flcidc  40118  iocmbl  40163  arearect  40165  iscard4  40241  briunov2uz  40399  eliunov2uz  40400  frege124d  40462  frege129d  40464  frege92  40656  lhe4.4ex1a  41033  dvconstbi  41038  binomcxplemnn0  41053  binomcxplemnotnn0  41060  infxr  41999  infleinflem2  42003  climneg  42252  cncfiooicc  42536  itgsinexplem1  42596  volioof  42629  stoweidlem36  42678  wallispilem3  42709  fourierdlem93  42841  fouriersw  42873  fouriercn  42874  etransclem16  42892  etransclem33  42909  sge0reuz  43086  nnfoctbdjlem  43094  hoidmvlelem3  43236  dfatafv2ex  43769  sprsymrelfvlem  44007  fmtnofz04prm  44094  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  lincext2  44864  blennn0elnn  44991  itcovalsucov  45082