Theorem eqeltrdi 2873

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eqeltrrdi  2874  csbexg  5275  unisn2  5277  class2set  5327  snexALT  5356  snexOLD  5415  prexOLD  5416  iotaex  6516  fvrn0  6913  f0cli  7097  funsneqopb  7155  fmptsng  7172  fmptsnd  7173  elimdelov  7515  ovima0  7599  ndmovcl  7605  caovmo  7657  soex  7924  zfrep6OLD  7958  1st2ndb  8032  fprresex  8313  smofvon2  8349  tz7.44-2  8400  oesuclem  8516  omcl  8527  oecl  8528  nnmcl  8604  nnecl  8605  fsetex  8859  fsetexb  8867  ixpexg  8926  resixpfo  8940  xpsnen  9056  ssfi  9164  cnvfi  9167  nnunifi  9258  prfi  9290  fsuppun  9354  0fsupp  9357  oiexg  9504  hartogslem1  9511  cantnfvalf  9641  rnttrcl  9698  ttrclse  9703  rankdmr1  9780  rankr1c  9800  numwdom  10059  alephon  10069  isfin5  10298  sdom2en01  10301  isf32lem9  10360  hsmexlem9  10424  iundom2g  10539  gchxpidm  10669  r1tskina  10782  tskmcl  10841  recmulnq  10964  recclnq  10966  genpelv  11000  un0mulcl  12553  znegcl  12644  zeo  12698  eqreznegel  12974  xnegcl  13255  xnn0xaddcl  13277  ioorebas  13494  modid0  13948  2txmodxeq0  13985  fzofi  14028  seqexw  14071  expcllem  14126  m1expcl2  14139  faclbnd4lem3  14349  bccl  14376  hasheq0  14417  hashrabrsn  14426  fnfz0hashnn0  14503  fnfzo0hashnn0  14506  wrdnfi  14603  cshwcl  14859  relexpaddg  15114  sgncl  15158  abs00bd  15366  iserge0  15736  sumrblem  15785  fsumcvg  15786  summolem2a  15789  sumss  15798  fsumss  15799  fsumcvg2  15801  sumsplit  15842  binom  15907  bcxmas  15912  geomulcvg  15953  prodrblem  16006  fprodcvg  16007  prodmolem2a  16011  zprod  16014  fprodntriv  16019  prodss  16024  fprodss  16025  binomfallfac  16117  bpoly1  16127  bpoly2  16133  bpoly3  16134  ruclem6  16313  smupf  16558  gcdcl  16586  lcmcl  16681  lcmfcl  16708  2mulprm  16773  pcxnn0cl  16942  pcxcl  16943  pcmptcl  16973  infpnlem2  16993  zgz  17015  4sqlem2  17031  4sqlem19  17045  vdwapval  17055  hashbc0  17087  ramcl2  17098  0ramcl  17105  ramcl  17111  isstruct2  17231  imasval  17587  imasbas  17588  imasds  17589  imasplusg  17593  imasmulr  17594  imasvsca  17596  imasip  17597  imasle  17599  qusaddvallem  17627  qusaddflem  17628  qusaddval  17629  qusaddf  17630  qusmulval  17631  qusmulf  17632  mreexexlem3d  17724  sscpwex  17894  fullresc  17930  estrres  18217  evlfcl  18300  ipopos  18614  gsumress  18772  submnd0OLD  18858  qusgrp2  19168  mulgfval  19179  issubg2  19252  triv1nsgd  19283  0subgALT  19682  torsubg  19968  frgpnabllem1  19987  lt6abl  20009  ablfaclem3  20203  ablfac2  20205  simpgnsgd  20216  qusrng  20302  srgbinomlem3  20354  ringidss  20405  qusring2  20462  isdrngd  20918  isdrngdOLD  20920  mptscmfsupp0  21098  islss3  21130  ellspsn  21174  lspprel  21265  znf1o  21751  frgpcyg  21773  cnmsgnsubg  21777  phlpropd  21855  cssval  21882  iscss  21883  dsmm0cl  21940  uvcvvcl  21987  m1detdiag  22804  m2detleiblem1  22831  pmatcollpw3fi1lem1  22993  indistopon  23208  indiscld  23298  restbas  23365  ordttopon  23400  iocpnfordt  23422  icomnfordt  23423  lecldbas  23426  fiuncmp  23611  cmpfi  23615  conncompid  23638  dissnlocfin  23737  elpt  23780  xkotop  23796  xkouni  23807  xkohaus  23861  xkoptsub  23862  imastopn  23928  filconn  24091  cfinufil  24136  alexsublem  24252  alexsub  24253  alexsubALTlem4  24258  distgp  24307  indistgp  24308  ssblps  24630  ssbl  24631  xmeter  24641  nmoi  24936  nmoeq0  24944  0nghm  24949  idnghm  24951  icccld  24974  iocmnfcld  24976  blssioo  25003  xrtgioo  25015  xrsxmet  25018  icccmp  25034  pcopt  25232  pcopt2  25233  elpi1  25255  cmetcaulem  25498  ishl2  25580  rrxmvallem  25614  ovolcl  25688  ovolunlem1a  25706  ovolunnul  25710  ovoliunnul  25717  ioombl1  25772  icombl  25774  ioombl  25775  iccmbl  25776  iccvolcl  25777  ovolioo  25778  ioovolcl  25780  ioorcl  25787  uniioovol  25789  uniioombllem2a  25792  uniioombllem4  25796  uniioombllem5  25797  vitalilem1  25818  vitalilem5  25822  mbfconstlem  25837  mbfima  25840  mbfid  25845  ismbf2d  25850  mbfss  25856  mbfmulc2lem  25857  i1fd  25891  itg1addlem2  25907  itg1addlem4  25909  itg1addlem5  25910  i1fmulc  25913  itg2l  25939  itg2cl  25942  ibl0  25997  iblrelem  26001  iblpos  26003  iblss2  26016  bddmulibl  26049  bddiblnc  26052  recnperf  26115  ply1remlem  26373  fta1glem1  26376  fta1g  26378  elply  26403  plypf1  26420  coefv0  26456  coemulc  26463  fta1  26520  elqaalem2  26532  aannenlem2  26543  aalioulem3  26548  taylfvallem1  26571  tayl0  26576  ulm0  26605  logtayl  26876  atanrecl  27127  atanbnd  27142  harmonicbnd3  27223  ftalem7  27294  basellem5  27300  ppifi  27321  sqff1o  27397  1sgmprm  27414  logexprlim  27440  dchrelbasd  27454  dchr1re  27478  lgslem4  27515  lgsne0  27550  2sqlem9  27642  2sqlem10  27643  rpvmasumlem  27702  dchrisumlem1  27704  vmalogdivsum  27754  pntrlog2bndlem5  27796  ostth  27854  lrrecse  28186  sltmuls1  28391  sltmuls2  28392  mulsuniflem  28393  noseqex  28533  n0mulscl  28589  n0fincut  28599  eln0s  28605  n0subs  28607  n0zs  28633  expscllem  28674  elz12s  28716  tgcgr4  28851  axlowdimlem16  29362  fusgrfisbase  29736  vtxdg0e  29882  rgrusgrprc  29997  wwlksnfi  30322  trlsegvdeglem7  30648  eulerpathpr  30662  0blo  31215  nmlno0lem  31216  omlsilem  31825  pjoc1i  31854  nonbooli  32074  nmlnop0iALT  32418  unopbd  32438  leoprf2  32550  opsqrlem4  32566  opsqrlem5  32567  pjbdlni  32572  pjcmul1i  32624  mptiffisupp  33109  drngidlhash  33805  evl1deg1  33930  ply1dg1rt  33934  ply1dg3rt0irred  33938  m1pmeq  33939  mplmulmvr  33993  esplyfvaln  34028  vieta  34034  lvecendof1f1o  34087  fldext2rspun  34136  constrabscl  34232  zarcmplem  34335  prsssdm  34371  ordtrestNEW  34375  esumpad  34509  esumpad2  34510  esumcst  34517  esumrnmpt2  34522  sibf0  34789  sitgclcn  34799  sitgclre  34800  eulerpartlemgs2  34835  dstfrvclim1  34933  ballotlemfelz  34946  signstfveq0  35029  breprexp  35085  r1wf  35547  fineqvnttrclselem1  35591  wevgblacfn  35652  subfacp1lem3  35711  rellysconn  35780  cvmlift2lem9  35840  nnuni  36256  ordcmp  37015  bj-snex  37728  finxpreclem4  38097  poimirlem16  38344  poimirlem17  38345  voliunnfl  38372  mbfresfi  38374  itg2addnclem2  38380  dvasin  38412  heiborlem4  38523  heiborlem6  38525  25or6to4  43031  itrere  43137  sn-itrere  43320  sn-retire  43321  wepwsolem  43827  flcidc  43955  iocmbl  43998  arearect  44000  omcl3g  44119  iscard4  44317  briunov2uz  44482  eliunov2uz  44483  frege124d  44545  frege129d  44547  frege92  44739  lhe4.4ex1a  45097  dvconstbi  45102  binomcxplemnn0  45117  binomcxplemnotnn0  45124  infxr  46140  infleinflem2  46144  climneg  46384  cncfiooicc  46666  itgsinexplem1  46726  volioof  46759  stoweidlem36  46808  wallispilem3  46839  fourierdlem93  46971  fouriersw  47003  fouriercn  47004  etransclem16  47022  etransclem33  47039  sge0reuz  47219  nnfoctbdjlem  47227  hoidmvlelem3  47369  sqrtqaa  47664  sinnpoly  47686  dfatafv2ex  48008  sprsymrelfvlem  48297  fmtnofz04prm  48387  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  gpg3nbgrvtx0  48899  lincext2  49292  blennn0elnn  49414  itcovalsucov  49505  resccat  49909  funcf2lem2  49917  isnatd  50058  swapfelvv  50098  fucoelvv  50155  prcofelvv  50215  termco  50316  prstcprs  50395