Theorem eqeltrdi 2834

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803

This theorem is referenced by:  eqeltrrdi  2835  csbexg  5307  unisn2  5309  class2set  5351  snexALT  5379  snex  5429  prex  5430  iotaex  6519  iotaexOLD  6526  fvrn0  6923  f0cli  7104  funsneqopb  7158  fmptsng  7174  fmptsnd  7175  elimdelov  7513  ovima0  7597  ndmovcl  7603  caovmo  7655  soex  7926  zfrep6  7960  1st2ndb  8035  fprresex  8317  wfrlem17OLD  8347  smofvon2  8378  tz7.44-2  8429  oesuclem  8547  omcl  8558  oecl  8559  nnmcl  8634  nnecl  8635  fsetex  8877  fsetexb  8885  ixpexg  8943  resixpfo  8957  en1bOLD  9052  xpsnen  9085  ssfi  9204  cnvfi  9207  nnunifi  9321  imafiOLD  9349  xpfiOLD  9354  prfi  9358  fsuppun  9423  0fsupp  9426  oiexg  9571  hartogslem1  9578  cantnfvalf  9701  rnttrcl  9758  ttrclse  9763  rankdmr1  9837  rankr1c  9857  numwdom  10095  alephon  10105  isfin5  10333  sdom2en01  10336  isf32lem9  10395  hsmexlem9  10459  iundom2g  10574  gchxpidm  10703  r1tskina  10816  tskmcl  10875  recmulnq  10998  recclnq  11000  genpelv  11034  un0mulcl  12552  znegcl  12643  zeo  12694  eqreznegel  12964  xnegcl  13240  xnn0xaddcl  13262  ioorebas  13476  modid0  13911  2txmodxeq0  13945  fzofi  13988  seqexw  14031  expcllem  14086  m1expcl2  14099  faclbnd4lem3  14307  bccl  14334  hasheq0  14375  hashrabrsn  14384  fnfz0hashnn0  14460  fnfzo0hashnn0  14463  wrdnfi  14551  cshwcl  14801  relexpaddg  15053  abs00bd  15291  iserge0  15660  sumrblem  15710  fsumcvg  15711  summolem2a  15714  sumss  15723  fsumss  15724  fsumcvg2  15726  sumsplit  15767  binom  15829  bcxmas  15834  geomulcvg  15875  prodrblem  15926  fprodcvg  15927  prodmolem2a  15931  zprod  15934  fprodntriv  15939  prodss  15944  fprodss  15945  binomfallfac  16038  bpoly1  16048  bpoly2  16054  bpoly3  16055  ruclem6  16232  smupf  16473  gcdcl  16501  lcmcl  16597  lcmfcl  16624  2mulprm  16689  pcxnn0cl  16857  pcxcl  16858  pcmptcl  16888  infpnlem2  16908  zgz  16930  4sqlem2  16946  4sqlem19  16960  vdwapval  16970  hashbc0  17002  ramcl2  17013  0ramcl  17020  ramcl  17026  isstruct2  17146  imasval  17521  imasbas  17522  imasds  17523  imasplusg  17527  imasmulr  17528  imasvsca  17530  imasip  17531  imasle  17533  qusaddvallem  17561  qusaddflem  17562  qusaddval  17563  qusaddf  17564  qusmulval  17565  qusmulf  17566  mreexexlem3d  17654  sscpwex  17826  fullresc  17865  estrres  18158  evlfcl  18242  ipopos  18556  gsumress  18670  submnd0  18751  qusgrp2  19048  mulgfval  19059  issubg2  19131  triv1nsgd  19163  0subgALT  19562  torsubg  19848  frgpnabllem1  19867  lt6abl  19889  ablfaclem3  20083  ablfac2  20085  simpgnsgd  20096  qusrng  20159  srgbinomlem3  20207  ringidss  20252  qusring2  20309  isdrngd  20739  isdrngdOLD  20741  mptscmfsupp0  20899  islss3  20932  ellspsn  20976  lspprel  21068  znf1o  21545  frgpcyg  21567  cnmsgnsubg  21569  phlpropd  21647  cssval  21674  iscss  21675  dsmm0cl  21734  uvcvvcl  21781  m1detdiag  22587  m2detleiblem1  22614  pmatcollpw3fi1lem1  22776  indistopon  22992  indiscld  23083  restbas  23150  ordttopon  23185  iocpnfordt  23207  icomnfordt  23208  lecldbas  23211  fiuncmp  23396  cmpfi  23400  conncompid  23423  dissnlocfin  23521  elpt  23564  xkotop  23580  xkouni  23591  xkohaus  23645  xkoptsub  23646  imastopn  23712  filconn  23875  cfinufil  23920  alexsublem  24036  alexsub  24037  alexsubALTlem4  24042  distgp  24091  indistgp  24092  ssblps  24416  ssbl  24417  xmeter  24427  nmoi  24733  nmoeq0  24741  0nghm  24746  idnghm  24748  icccld  24771  iocmnfcld  24773  blssioo  24799  xrtgioo  24810  xrsxmet  24813  icccmp  24829  pcopt  25037  pcopt2  25038  elpi1  25060  cmetcaulem  25304  ishl2  25386  rrxmvallem  25420  ovolcl  25495  ovolunlem1a  25513  ovolunnul  25517  ovoliunnul  25524  ioombl1  25579  icombl  25581  ioombl  25582  iccmbl  25583  iccvolcl  25584  ovolioo  25585  ioovolcl  25587  ioorcl  25594  uniioovol  25596  uniioombllem2a  25599  uniioombllem4  25603  uniioombllem5  25604  vitalilem1  25625  vitalilem5  25629  mbfconstlem  25644  mbfima  25647  mbfid  25652  ismbf2d  25657  mbfss  25663  mbfmulc2lem  25664  i1fd  25698  itg1addlem2  25714  itg1addlem4  25716  itg1addlem4OLD  25717  itg1addlem5  25718  i1fmulc  25721  itg2l  25747  itg2cl  25750  ibl0  25804  iblrelem  25808  iblpos  25810  iblss2  25823  bddmulibl  25856  bddiblnc  25859  recnperf  25922  ply1remlem  26189  fta1glem1  26192  fta1g  26194  elply  26219  plypf1  26236  coefv0  26272  coemulc  26279  fta1  26333  elqaalem2  26345  aannenlem2  26354  aalioulem3  26359  taylfvallem1  26381  tayl0  26386  ulm0  26417  logtayl  26684  atanrecl  26936  atanbnd  26951  harmonicbnd3  27033  ftalem7  27104  basellem5  27110  ppifi  27131  sqff1o  27207  1sgmprm  27225  logexprlim  27251  dchrelbasd  27265  dchr1re  27289  lgslem4  27326  lgsne0  27361  2sqlem9  27453  2sqlem10  27454  rpvmasumlem  27513  dchrisumlem1  27515  vmalogdivsum  27565  pntrlog2bndlem5  27607  ostth  27665  lrrecse  27953  ssltmul1  28145  ssltmul2  28146  mulsuniflem  28147  noseqex  28260  n0mulscl  28311  eln0s  28321  n0subs  28323  n0zs  28335  tgcgr4  28455  axlowdimlem16  28888  fusgrfisbase  29261  vtxdg0e  29408  rgrusgrprc  29523  wwlksnfi  29837  trlsegvdeglem7  30156  eulerpathpr  30170  0blo  30722  nmlno0lem  30723  omlsilem  31332  pjoc1i  31361  nonbooli  31581  nmlnop0iALT  31925  unopbd  31945  leoprf2  32057  opsqrlem4  32073  opsqrlem5  32074  pjbdlni  32079  pjcmul1i  32131  mptiffisupp  32605  drngidlhash  33315  evl1deg1  33454  ply1dg1rt  33457  ply1dg3rt0irred  33460  m1pmeq  33461  zarcmplem  33709  prsssdm  33745  ordtrestNEW  33749  esumpad  33901  esumpad2  33902  esumcst  33909  esumrnmpt2  33914  sibf0  34181  sitgclcn  34191  sitgclre  34192  eulerpartlemgs2  34227  dstfrvclim1  34324  ballotlemfelz  34337  sgncl  34385  signstfveq0  34436  breprexp  34492  wevgblacfn  34949  subfacp1lem3  35023  rellysconn  35092  cvmlift2lem9  35152  nnuni  35562  ordcmp  36172  bj-snex  36755  finxpreclem4  37114  poimirlem16  37350  poimirlem17  37351  voliunnfl  37378  mbfresfi  37380  itg2addnclem2  37386  dvasin  37418  heiborlem4  37528  heiborlem6  37530  itrere  42046  sn-itrere  42179  sn-retire  42180  wepwsolem  42740  flcidc  42872  iocmbl  42915  arearect  42917  omcl3g  43037  iscard4  43237  briunov2uz  43402  eliunov2uz  43403  frege124d  43465  frege129d  43467  frege92  43659  lhe4.4ex1a  44040  dvconstbi  44045  binomcxplemnn0  44060  binomcxplemnotnn0  44067  infxr  45018  infleinflem2  45022  climneg  45267  cncfiooicc  45551  itgsinexplem1  45611  volioof  45644  stoweidlem36  45693  wallispilem3  45724  fourierdlem93  45856  fouriersw  45888  fouriercn  45889  etransclem16  45907  etransclem33  45924  sge0reuz  46104  nnfoctbdjlem  46112  hoidmvlelem3  46254  upwordnul  46535  dfatafv2ex  46862  sprsymrelfvlem  47098  fmtnofz04prm  47185  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  lincext2  47874  blennn0elnn  48001  itcovalsucov  48092  prstcprs  48432