Theorem eqeltrdi 2872

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqeltrrdi  2873  csbexg  5270  unisn2  5272  class2set  5323  snexALT  5352  snexOLD  5407  prexOLD  5408  iotaex  6541  fvrn0  6944  f0cli  7130  funsneqopb  7188  fmptsng  7204  fmptsnd  7205  elimdelov  7547  ovima0  7632  ndmovcl  7638  caovmo  7690  soex  7967  zfrep6OLD  8001  1st2ndb  8075  fprresex  8366  smofvon2  8402  tz7.44-2  8453  oesuclem  8571  omcl  8582  oecl  8583  nnmcl  8659  nnecl  8660  fsetex  8916  fsetexb  8924  ixpexg  8988  resixpfo  9002  xpsnen  9118  ssfi  9226  cnvfi  9229  nnunifi  9321  prfi  9353  fsuppun  9416  0fsupp  9419  oiexg  9566  hartogslem1  9573  cantnfvalf  9703  rnttrcl  9760  ttrclse  9765  rankdmr1  9846  rankr1c  9867  r1wf  9878  numwdom  10177  alephon  10187  isfin5  10416  sdom2en01  10419  isf32lem9  10478  hsmexlem9  10542  iundom2g  10663  gchxpidm  10793  r1tskina  10906  tskmcl  10965  recmulnq  11088  recclnq  11090  genpelv  11124  un0mulcl  12680  znegcl  12771  zeo  12825  eqreznegel  13101  xnegcl  13383  xnn0xaddcl  13405  ioorebas  13622  modid0  14077  2txmodxeq0  14114  fzofi  14157  seqexw  14200  expcllem  14255  m1expcl2  14268  faclbnd4lem3  14480  bccl  14507  hasheq0  14548  hashrabrsn  14557  fnfz0hashnn0  14634  fnfzo0hashnn0  14637  wrdnfi  14734  cshwcl  14991  relexpaddg  15249  sgncl  15293  abs00bd  15501  iserge0  15872  sumrblem  15921  fsumcvg  15922  summolem2a  15925  sumss  15934  fsumss  15935  fsumcvg2  15937  sumsplit  15978  binom  16043  bcxmas  16048  geomulcvg  16089  prodrblem  16140  fprodcvg  16141  prodmolem2a  16145  zprod  16148  fprodntriv  16153  prodss  16158  fprodss  16159  binomfallfac  16251  bpoly1  16261  bpoly2  16267  bpoly3  16268  ruclem6  16447  smupf  16692  gcdcl  16720  lcmcl  16820  lcmfcl  16847  2mulprm  16912  pcxnn0cl  17082  pcxcl  17083  pcmptcl  17113  infpnlem2  17133  zgz  17155  4sqlem2  17171  4sqlem19  17185  vdwapval  17195  hashbc0  17227  ramcl2  17238  0ramcl  17245  ramcl  17251  isstruct2  17371  imasval  17733  imasbas  17734  imasds  17735  imasplusg  17739  imasmulr  17740  imasvsca  17742  imasip  17743  imasle  17745  qusaddvallem  17773  qusaddflem  17774  qusaddval  17775  qusaddf  17776  qusmulval  17777  qusmulf  17778  mreexexlem3d  17870  sscpwex  18040  fullresc  18076  estrres  18363  evlfcl  18446  ipopos  18760  imasmgm2  18913  qusmgm  18914  gsumress  18921  submnd0OLD  19007  qusmnd  19025  qusgrp2  19318  mulgfval  19329  issubg2  19402  triv1nsgd  19433  0subgALT  19833  torsubg  20119  frgpnabllem1  20138  lt6abl  20160  ablfaclem3  20354  ablfac2  20356  simpgnsgd  20367  qusrng  20453  srgbinomlem3  20505  ringidss  20557  qusring2  20615  isdrngd  21073  isdrngdOLD  21075  mptscmfsupp0  21253  islss3  21285  ellspsn  21329  lspprel  21420  znf1o  21912  frgpcyg  21934  cnmsgnsubg  21938  phlpropd  22016  cssval  22043  iscss  22044  dsmm0cl  22101  uvcvvcl  22148  m1detdiag  22967  m2detleiblem1  22994  pmatcollpw3fi1lem1  23159  indistopon  23374  indiscld  23464  restbas  23531  ordttopon  23566  iocpnfordt  23588  icomnfordt  23589  lecldbas  23592  fiuncmp  23777  cmpfi  23781  conncompid  23804  dissnlocfin  23903  elpt  23946  xkotop  23962  xkouni  23973  xkohaus  24027  xkoptsub  24028  imastopn  24094  filconn  24257  cfinufil  24302  alexsublem  24418  alexsub  24419  alexsubALTlem4  24424  distgp  24473  indistgp  24474  ssblps  24796  ssbl  24797  xmeter  24807  nmoi  25102  nmoeq0  25110  0nghm  25115  idnghm  25117  icccld  25140  iocmnfcld  25142  blssioo  25169  xrtgioo  25181  xrsxmet  25184  icccmp  25200  pcopt  25398  pcopt2  25399  elpi1  25421  cmetcaulem  25664  ishl2  25746  rrxmvallem  25780  ovolcl  25854  ovolunlem1a  25872  ovolunnul  25876  ovoliunnul  25883  ioombl1  25938  icombl  25940  ioombl  25941  iccmbl  25942  iccvolcl  25943  ovolioo  25944  ioovolcl  25946  ioorcl  25953  uniioovol  25955  uniioombllem2a  25958  uniioombllem4  25962  uniioombllem5  25963  vitalilem1  25984  vitalilem5  25988  mbfconstlem  26003  mbfima  26006  mbfid  26011  ismbf2d  26016  mbfss  26022  mbfmulc2lem  26023  i1fd  26057  itg1addlem2  26073  itg1addlem4  26075  itg1addlem5  26076  i1fmulc  26079  itg2l  26105  itg2cl  26108  ibl0  26162  iblrelem  26166  iblpos  26168  iblss2  26181  bddmulibl  26214  bddiblnc  26217  recnperf  26280  ply1remlem  26538  fta1glem1  26541  fta1g  26543  elply  26568  plypf1  26586  coefv0  26622  coemulc  26629  fta1  26684  elqaalem2  26700  aannenlem2  26713  aalioulem3  26718  taylfvallem1  26741  tayl0  26746  ulm0  26775  logtayl  27045  atanrecl  27296  atanbnd  27311  harmonicbnd3  27392  ftalem7  27463  basellem5  27469  ppifi  27490  sqff1o  27566  1sgmprm  27583  logexprlim  27609  dchrelbasd  27623  dchr1re  27647  lgslem4  27684  lgsne0  27719  2sqlem9  27811  2sqlem10  27812  rpvmasumlem  27871  dchrisumlem1  27873  vmalogdivsum  27923  pntrlog2bndlem5  27965  ostth  28023  lrrecse  28385  sltmuls1  28590  sltmuls2  28591  mulsuniflem  28592  noseqex  28732  n0mulscl  28788  n0fincut  28798  eln0s  28804  n0subs  28806  n0zs  28832  expscllem  28873  elz12s  28915  tgcgr4  29051  axlowdimlem16  29592  fusgrfisbase  29966  vtxdg0e  30112  rgrusgrprc  30227  wwlksnfi  30552  trlsegvdeglem7  30884  eulerpathpr  30898  0blo  31451  nmlno0lem  31452  omlsilem  32061  pjoc1i  32090  nonbooli  32310  nmlnop0iALT  32654  unopbd  32674  leoprf2  32786  opsqrlem4  32802  opsqrlem5  32803  pjbdlni  32808  pjcmul1i  32860  mptiffisupp  33383  drngidlhash  34087  evl1deg1  34211  ply1dg1rt  34215  ply1dg3rt0irred  34219  m1pmeq  34220  rngunsnply1chr2lem2  34251  mplmulmvr  34282  esplyfvaln  34317  vieta  34323  lvecendof1f1o  34376  fldext2rspun  34425  constrabscl  34521  zarcmplem  34624  prsssdm  34660  ordtrestNEW  34664  esumpad  34798  esumpad2  34799  esumcst  34806  esumrnmpt2  34811  sibf0  35077  sitgclcn  35087  sitgclre  35088  eulerpartlemgs2  35123  dstfrvclim1  35221  ballotlemfelz  35234  signstfveq0  35317  breprexp  35373  fineqvnttrclselem1  35930  k1on  36056  k2on  36057  k39o  36058  wevgblacfn  36080  subfacp1lem3  36155  rellysconn  36224  cvmlift2lem9  36284  nnuni  36707  ordcmp  37450  bj-snex  38163  finxpreclem4  38585  poimirlem16  38822  poimirlem17  38823  voliunnfl  38850  mbfresfi  38852  itg2addnclem2  38858  dvasin  38890  heiborlem4  39014  heiborlem6  39016  25or6to4  43522  itrere  43641  sn-itrere  43818  sn-retire  43819  wepwsolem  44315  flcidc  44433  iocmbl  44476  arearect  44478  omcl3g  44597  iscard4  44795  briunov2uz  44959  eliunov2uz  44960  frege124d  45022  frege129d  45024  frege92  45216  lhe4.4ex1a  45574  dvconstbi  45579  binomcxplemnn0  45594  binomcxplemnotnn0  45601  mpoexwd  46187  infxr  46651  infleinflem2  46655  climneg  46895  cncfiooicc  47177  itgsinexplem1  47237  volioof  47270  stoweidlem36  47319  wallispilem3  47350  fourierdlem93  47482  fouriersw  47514  fouriercn  47515  etransclem16  47533  etransclem33  47550  sge0reuz  47730  nnfoctbdjlem  47738  hoidmvlelem3  47880  sqrtqaa  48188  sinnpoly  48214  tmachlem-extapes  48217  tmachlem-agreefin  48231  dfatafv2ex  48556  sprsymrelfvlem  48845  fmtnofz04prm  48935  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  gpg3nbgrvtx0  49447  lincext2  49898  blennn0elnn  50020  itcovalsucov  50111  resccat  50519  funcf2lem2  50527  isnatd  50670  swapfelvv  50716  fucoelvv  50773  prcofelvv  50846  termco  50947  prstcprs  51029  parswapprop  51108