Theorem eqeltrdi 2868

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  eqeltrrdi  2869  csbexg  5263  unisn2  5265  class2set  5316  snexALT  5345  snexOLD  5400  prexOLD  5401  iotaex  6518  fvrn0  6918  f0cli  7103  funsneqopb  7161  fmptsng  7177  fmptsnd  7178  elimdelov  7520  ovima0  7604  ndmovcl  7610  caovmo  7662  soex  7937  zfrep6OLD  7971  1st2ndb  8045  fprresex  8336  smofvon2  8372  tz7.44-2  8423  oesuclem  8541  omcl  8552  oecl  8553  nnmcl  8629  nnecl  8630  fsetex  8886  fsetexb  8894  ixpexg  8958  resixpfo  8972  xpsnen  9088  ssfi  9196  cnvfi  9199  nnunifi  9291  prfi  9323  fsuppun  9386  0fsupp  9389  oiexg  9536  hartogslem1  9543  cantnfvalf  9673  rnttrcl  9730  ttrclse  9735  rankdmr1  9816  rankr1c  9837  r1wf  9848  numwdom  10145  alephon  10155  isfin5  10384  sdom2en01  10387  isf32lem9  10446  hsmexlem9  10510  iundom2g  10631  gchxpidm  10761  r1tskina  10874  tskmcl  10933  recmulnq  11056  recclnq  11058  genpelv  11092  un0mulcl  12647  znegcl  12738  zeo  12792  eqreznegel  13068  xnegcl  13350  xnn0xaddcl  13372  ioorebas  13589  modid0  14044  2txmodxeq0  14081  fzofi  14124  seqexw  14167  expcllem  14222  m1expcl2  14235  faclbnd4lem3  14446  bccl  14473  hasheq0  14514  hashrabrsn  14523  fnfz0hashnn0  14600  fnfzo0hashnn0  14603  wrdnfi  14700  cshwcl  14957  relexpaddg  15215  sgncl  15259  abs00bd  15467  iserge0  15837  sumrblem  15886  fsumcvg  15887  summolem2a  15890  sumss  15899  fsumss  15900  fsumcvg2  15902  sumsplit  15943  binom  16008  bcxmas  16013  geomulcvg  16054  prodrblem  16105  fprodcvg  16106  prodmolem2a  16110  zprod  16113  fprodntriv  16118  prodss  16123  fprodss  16124  binomfallfac  16216  bpoly1  16226  bpoly2  16232  bpoly3  16233  ruclem6  16412  smupf  16657  gcdcl  16685  lcmcl  16785  lcmfcl  16812  2mulprm  16877  pcxnn0cl  17047  pcxcl  17048  pcmptcl  17078  infpnlem2  17098  zgz  17120  4sqlem2  17136  4sqlem19  17150  vdwapval  17160  hashbc0  17192  ramcl2  17203  0ramcl  17210  ramcl  17216  isstruct2  17336  imasval  17692  imasbas  17693  imasds  17694  imasplusg  17698  imasmulr  17699  imasvsca  17701  imasip  17702  imasle  17704  qusaddvallem  17732  qusaddflem  17733  qusaddval  17734  qusaddf  17735  qusmulval  17736  qusmulf  17737  mreexexlem3d  17829  sscpwex  17999  fullresc  18035  estrres  18322  evlfcl  18405  ipopos  18719  imasmgm2  18872  qusmgm  18873  gsumress  18880  submnd0OLD  18966  qusmnd  18984  qusgrp2  19277  mulgfval  19288  issubg2  19361  triv1nsgd  19392  0subgALT  19791  torsubg  20077  frgpnabllem1  20096  lt6abl  20118  ablfaclem3  20312  ablfac2  20314  simpgnsgd  20325  qusrng  20411  srgbinomlem3  20463  ringidss  20515  qusring2  20573  isdrngd  21031  isdrngdOLD  21033  mptscmfsupp0  21211  islss3  21243  ellspsn  21287  lspprel  21378  znf1o  21866  frgpcyg  21888  cnmsgnsubg  21892  phlpropd  21970  cssval  21997  iscss  21998  dsmm0cl  22055  uvcvvcl  22102  m1detdiag  22921  m2detleiblem1  22948  pmatcollpw3fi1lem1  23113  indistopon  23328  indiscld  23418  restbas  23485  ordttopon  23520  iocpnfordt  23542  icomnfordt  23543  lecldbas  23546  fiuncmp  23731  cmpfi  23735  conncompid  23758  dissnlocfin  23857  elpt  23900  xkotop  23916  xkouni  23927  xkohaus  23981  xkoptsub  23982  imastopn  24048  filconn  24211  cfinufil  24256  alexsublem  24372  alexsub  24373  alexsubALTlem4  24378  distgp  24427  indistgp  24428  ssblps  24750  ssbl  24751  xmeter  24761  nmoi  25056  nmoeq0  25064  0nghm  25069  idnghm  25071  icccld  25094  iocmnfcld  25096  blssioo  25123  xrtgioo  25135  xrsxmet  25138  icccmp  25154  pcopt  25352  pcopt2  25353  elpi1  25375  cmetcaulem  25618  ishl2  25700  rrxmvallem  25734  ovolcl  25808  ovolunlem1a  25826  ovolunnul  25830  ovoliunnul  25837  ioombl1  25892  icombl  25894  ioombl  25895  iccmbl  25896  iccvolcl  25897  ovolioo  25898  ioovolcl  25900  ioorcl  25907  uniioovol  25909  uniioombllem2a  25912  uniioombllem4  25916  uniioombllem5  25917  vitalilem1  25938  vitalilem5  25942  mbfconstlem  25957  mbfima  25960  mbfid  25965  ismbf2d  25970  mbfss  25976  mbfmulc2lem  25977  i1fd  26011  itg1addlem2  26027  itg1addlem4  26029  itg1addlem5  26030  i1fmulc  26033  itg2l  26059  itg2cl  26062  ibl0  26116  iblrelem  26120  iblpos  26122  iblss2  26135  bddmulibl  26168  bddiblnc  26171  recnperf  26234  ply1remlem  26492  fta1glem1  26495  fta1g  26497  elply  26522  plypf1  26540  coefv0  26576  coemulc  26583  fta1  26638  elqaalem2  26652  aannenlem2  26665  aalioulem3  26670  taylfvallem1  26693  tayl0  26698  ulm0  26727  logtayl  26997  atanrecl  27248  atanbnd  27263  harmonicbnd3  27344  ftalem7  27415  basellem5  27421  ppifi  27442  sqff1o  27518  1sgmprm  27535  logexprlim  27561  dchrelbasd  27575  dchr1re  27599  lgslem4  27636  lgsne0  27671  2sqlem9  27763  2sqlem10  27764  rpvmasumlem  27823  dchrisumlem1  27825  vmalogdivsum  27875  pntrlog2bndlem5  27917  ostth  27975  lrrecse  28337  sltmuls1  28542  sltmuls2  28543  mulsuniflem  28544  noseqex  28684  n0mulscl  28740  n0fincut  28750  eln0s  28756  n0subs  28758  n0zs  28784  expscllem  28825  elz12s  28867  tgcgr4  29003  axlowdimlem16  29544  fusgrfisbase  29918  vtxdg0e  30064  rgrusgrprc  30179  wwlksnfi  30504  trlsegvdeglem7  30836  eulerpathpr  30850  0blo  31403  nmlno0lem  31404  omlsilem  32013  pjoc1i  32042  nonbooli  32262  nmlnop0iALT  32606  unopbd  32626  leoprf2  32738  opsqrlem4  32754  opsqrlem5  32755  pjbdlni  32760  pjcmul1i  32812  mptiffisupp  33337  drngidlhash  34033  evl1deg1  34158  ply1dg1rt  34162  ply1dg3rt0irred  34166  m1pmeq  34167  mplmulmvr  34221  esplyfvaln  34256  vieta  34262  lvecendof1f1o  34315  fldext2rspun  34364  constrabscl  34460  zarcmplem  34563  prsssdm  34599  ordtrestNEW  34603  esumpad  34737  esumpad2  34738  esumcst  34745  esumrnmpt2  34750  sibf0  35016  sitgclcn  35026  sitgclre  35027  eulerpartlemgs2  35062  dstfrvclim1  35160  ballotlemfelz  35173  signstfveq0  35256  breprexp  35312  fineqvnttrclselem1  35857  k1on  35966  k2on  35967  k39o  35968  wevgblacfn  35990  subfacp1lem3  36065  rellysconn  36134  cvmlift2lem9  36194  nnuni  36616  ordcmp  37359  bj-snex  38072  finxpreclem4  38454  poimirlem16  38691  poimirlem17  38692  voliunnfl  38719  mbfresfi  38721  itg2addnclem2  38727  dvasin  38759  heiborlem4  38885  heiborlem6  38887  25or6to4  43393  itrere  43512  sn-itrere  43689  sn-retire  43690  wepwsolem  44186  flcidc  44309  iocmbl  44352  arearect  44354  omcl3g  44473  iscard4  44671  briunov2uz  44835  eliunov2uz  44836  frege124d  44898  frege129d  44900  frege92  45092  lhe4.4ex1a  45450  dvconstbi  45455  binomcxplemnn0  45470  binomcxplemnotnn0  45477  infxr  46514  infleinflem2  46518  climneg  46758  cncfiooicc  47040  itgsinexplem1  47100  volioof  47133  stoweidlem36  47182  wallispilem3  47213  fourierdlem93  47345  fouriersw  47377  fouriercn  47378  etransclem16  47396  etransclem33  47413  sge0reuz  47593  nnfoctbdjlem  47601  hoidmvlelem3  47743  sqrtqaa  48051  sinnpoly  48077  tmachlem-extapes  48080  tmachlem-agreefin  48094  dfatafv2ex  48419  sprsymrelfvlem  48708  fmtnofz04prm  48798  nnsum4primeseven  49034  nnsum4primesevenALTV  49035  gpg3nbgrvtx0  49310  lincext2  49703  blennn0elnn  49825  itcovalsucov  49916  resccat  50324  funcf2lem2  50332  isnatd  50475  swapfelvv  50521  fucoelvv  50578  prcofelvv  50651  termco  50752  prstcprs  50834  parswapprop  50913