Theorem eqeltrdi 2847

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  eqeltrrdi  2848  csbexg  5232  unisn2  5234  class2set  5274  snexALT  5304  snex  5352  prex  5353  iotaex  6406  fvrn0  6794  f0cli  6966  funsneqopb  7016  fmptsng  7032  fmptsnd  7033  elimdelov  7361  ovima0  7441  ndmovcl  7447  caovmo  7499  soex  7758  zfrep6  7787  1st2ndb  7860  fprresex  8113  wfrlem17OLD  8143  smofvon2  8174  tz7.44-2  8225  oesuclem  8342  omcl  8353  oecl  8354  nnmcl  8430  nnecl  8431  fsetex  8631  fsetexb  8639  ixpexg  8697  resixpfo  8711  en1bOLD  8801  xpsnen  8829  ssfi  8943  imafi  8945  cnvfi  8950  nnunifi  9052  xpfi  9072  fsuppun  9134  0fsupp  9137  oiexg  9281  hartogslem1  9288  cantnfvalf  9410  rnttrcl  9467  ttrclse  9472  rankdmr1  9569  rankr1c  9589  numwdom  9825  alephon  9835  isfin5  10065  sdom2en01  10068  isf32lem9  10127  hsmexlem9  10191  iundom2g  10306  gchxpidm  10435  r1tskina  10548  tskmcl  10607  recmulnq  10730  recclnq  10732  genpelv  10766  un0mulcl  12277  znegcl  12365  zeo  12416  eqreznegel  12684  xnegcl  12957  xnn0xaddcl  12979  ioorebas  13193  modid0  13627  2txmodxeq0  13661  fzofi  13704  seqexw  13747  expcllem  13803  m1expcl2  13814  faclbnd4lem3  14019  bccl  14046  hasheq0  14088  hashrabrsn  14097  fnfz0hashnn0  14170  fnfzo0hashnn0  14173  wrdnfi  14261  ccat2s1p1OLD  14348  cshwcl  14521  relexpaddg  14774  abs00bd  15013  iserge0  15382  sumrblem  15433  fsumcvg  15434  summolem2a  15437  sumss  15446  fsumss  15447  fsumcvg2  15449  sumsplit  15490  binom  15552  bcxmas  15557  geomulcvg  15598  prodrblem  15649  fprodcvg  15650  prodmolem2a  15654  zprod  15657  fprodntriv  15662  prodss  15667  fprodss  15668  binomfallfac  15761  bpoly1  15771  bpoly2  15777  bpoly3  15778  ruclem6  15954  smupf  16195  gcdcl  16223  lcmcl  16316  lcmfcl  16343  2mulprm  16408  pcxnn0cl  16571  pcxcl  16572  pcmptcl  16602  infpnlem2  16622  zgz  16644  4sqlem2  16660  4sqlem19  16674  vdwapval  16684  hashbc0  16716  ramcl2  16727  0ramcl  16734  ramcl  16740  isstruct2  16860  imasval  17232  imasbas  17233  imasds  17234  imasplusg  17238  imasmulr  17239  imasvsca  17241  imasip  17242  imasle  17244  qusaddvallem  17272  qusaddflem  17273  qusaddval  17274  qusaddf  17275  qusmulval  17276  qusmulf  17277  mreexexlem3d  17365  sscpwex  17537  fullresc  17576  estrres  17866  evlfcl  17950  ipopos  18264  gsumress  18376  submnd0  18424  qusgrp2  18703  mulgfval  18712  issubg2  18780  triv1nsgd  18811  torsubg  19465  frgpnabllem1  19484  lt6abl  19506  ablfaclem3  19700  ablfac2  19702  simpgnsgd  19713  srgbinomlem3  19788  ringidss  19826  qusring2  19869  isdrngd  20026  mptscmfsupp0  20198  islss3  20231  lspsnel  20275  lspprel  20366  znf1o  20769  frgpcyg  20791  cnmsgnsubg  20792  phlpropd  20870  cssval  20897  iscss  20898  dsmm0cl  20957  uvcvvcl  21004  m1detdiag  21756  m2detleiblem1  21783  pmatcollpw3fi1lem1  21945  indistopon  22161  indiscld  22252  restbas  22319  ordttopon  22354  iocpnfordt  22376  icomnfordt  22377  lecldbas  22380  fiuncmp  22565  cmpfi  22569  conncompid  22592  dissnlocfin  22690  elpt  22733  xkotop  22749  xkouni  22760  xkohaus  22814  xkoptsub  22815  imastopn  22881  filconn  23044  cfinufil  23089  alexsublem  23205  alexsub  23206  alexsubALTlem4  23211  distgp  23260  indistgp  23261  ssblps  23585  ssbl  23586  xmeter  23596  nmoi  23902  nmoeq0  23910  0nghm  23915  idnghm  23917  icccld  23940  iocmnfcld  23942  blssioo  23968  xrtgioo  23979  xrsxmet  23982  icccmp  23998  pcopt  24195  pcopt2  24196  elpi1  24218  cmetcaulem  24462  ishl2  24544  rrxmvallem  24578  ovolcl  24652  ovolunlem1a  24670  ovolunnul  24674  ovoliunnul  24681  ioombl1  24736  icombl  24738  ioombl  24739  iccmbl  24740  iccvolcl  24741  ovolioo  24742  ioovolcl  24744  ioorcl  24751  uniioovol  24753  uniioombllem2a  24756  uniioombllem4  24760  uniioombllem5  24761  vitalilem1  24782  vitalilem5  24786  mbfconstlem  24801  mbfima  24804  mbfid  24809  ismbf2d  24814  mbfss  24820  mbfmulc2lem  24821  i1fd  24855  itg1addlem2  24871  itg1addlem4  24873  itg1addlem4OLD  24874  itg1addlem5  24875  i1fmulc  24878  itg2l  24904  itg2cl  24907  ibl0  24961  iblrelem  24965  iblpos  24967  iblss2  24980  bddmulibl  25013  bddiblnc  25016  recnperf  25079  ply1remlem  25337  fta1glem1  25340  fta1g  25342  elply  25366  plypf1  25383  coefv0  25419  coemulc  25426  fta1  25478  elqaalem2  25490  aannenlem2  25499  aalioulem3  25504  taylfvallem1  25526  tayl0  25531  ulm0  25560  logtayl  25825  atanrecl  26071  atanbnd  26086  harmonicbnd3  26167  ftalem7  26238  basellem5  26244  ppifi  26265  sqff1o  26341  1sgmprm  26357  logexprlim  26383  dchrelbasd  26397  dchr1re  26421  lgslem4  26458  lgsne0  26493  2sqlem9  26585  2sqlem10  26586  rpvmasumlem  26645  dchrisumlem1  26647  vmalogdivsum  26697  pntrlog2bndlem5  26739  ostth  26797  tgcgr4  26902  axlowdimlem16  27335  fusgrfisbase  27705  vtxdg0e  27851  rgrusgrprc  27966  wwlksnfi  28279  trlsegvdeglem7  28598  eulerpathpr  28612  0blo  29162  nmlno0lem  29163  omlsilem  29772  pjoc1i  29801  nonbooli  30021  nmlnop0iALT  30365  unopbd  30385  leoprf2  30497  opsqrlem4  30513  opsqrlem5  30514  pjbdlni  30519  pjcmul1i  30571  zarcmplem  31839  prsssdm  31875  ordtrestNEW  31879  esumpad  32031  esumpad2  32032  esumcst  32039  esumrnmpt2  32044  sibf0  32309  sitgclcn  32319  sitgclre  32320  eulerpartlemgs2  32355  dstfrvclim1  32452  ballotlemfelz  32465  sgncl  32513  signstfveq0  32564  breprexp  32621  subfacp1lem3  33152  rellysconn  33221  cvmlift2lem9  33281  nnuni  33700  lrrecse  34107  ordcmp  34644  finxpreclem4  35573  poimirlem16  35801  poimirlem17  35802  voliunnfl  35829  mbfresfi  35831  itg2addnclem2  35837  dvasin  35869  heiborlem4  35980  heiborlem6  35982  sn-iotaex  40205  itrere  40444  retire  40445  wepwsolem  40875  flcidc  41007  iocmbl  41052  arearect  41054  iscard4  41130  briunov2uz  41287  eliunov2uz  41288  frege124d  41350  frege129d  41352  frege92  41544  lhe4.4ex1a  41928  dvconstbi  41933  binomcxplemnn0  41948  binomcxplemnotnn0  41955  infxr  42887  infleinflem2  42891  climneg  43132  cncfiooicc  43416  itgsinexplem1  43476  volioof  43509  stoweidlem36  43558  wallispilem3  43589  fourierdlem93  43721  fouriersw  43753  fouriercn  43754  etransclem16  43772  etransclem33  43789  sge0reuz  43966  nnfoctbdjlem  43974  hoidmvlelem3  44116  dfatafv2ex  44683  sprsymrelfvlem  44920  fmtnofz04prm  45007  nnsum4primeseven  45230  nnsum4primesevenALTV  45231  lincext2  45774  blennn0elnn  45901  itcovalsucov  45992  prstcprs  46334  upwordnul  46493