Theorem eqeltrdi 2845

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqeltrrdi  2846  csbexg  5245  unisn2  5247  class2set  5292  snexALT  5320  snexOLD  5379  prexOLD  5380  iotaex  6468  fvrn0  6862  f0cli  7044  funsneqopb  7099  fmptsng  7116  fmptsnd  7117  elimdelov  7456  ovima0  7539  ndmovcl  7545  caovmo  7597  soex  7865  zfrep6OLD  7901  1st2ndb  7975  fprresex  8253  smofvon2  8289  tz7.44-2  8339  oesuclem  8453  omcl  8464  oecl  8465  nnmcl  8541  nnecl  8542  fsetex  8796  fsetexb  8804  ixpexg  8863  resixpfo  8877  xpsnen  8992  ssfi  9100  cnvfi  9103  nnunifi  9194  imafiOLD  9219  prfi  9227  fsuppun  9293  0fsupp  9296  oiexg  9443  hartogslem1  9450  cantnfvalf  9577  rnttrcl  9634  ttrclse  9639  rankdmr1  9716  rankr1c  9736  numwdom  9972  alephon  9982  isfin5  10212  sdom2en01  10215  isf32lem9  10274  hsmexlem9  10338  iundom2g  10453  gchxpidm  10583  r1tskina  10696  tskmcl  10755  recmulnq  10878  recclnq  10880  genpelv  10914  un0mulcl  12462  znegcl  12553  zeo  12606  eqreznegel  12875  xnegcl  13156  xnn0xaddcl  13178  ioorebas  13395  modid0  13847  2txmodxeq0  13884  fzofi  13927  seqexw  13970  expcllem  14025  m1expcl2  14038  faclbnd4lem3  14248  bccl  14275  hasheq0  14316  hashrabrsn  14325  fnfz0hashnn0  14401  fnfzo0hashnn0  14404  wrdnfi  14501  cshwcl  14751  relexpaddg  15006  abs00bd  15244  iserge0  15614  sumrblem  15664  fsumcvg  15665  summolem2a  15668  sumss  15677  fsumss  15678  fsumcvg2  15680  sumsplit  15721  binom  15786  bcxmas  15791  geomulcvg  15832  prodrblem  15885  fprodcvg  15886  prodmolem2a  15890  zprod  15893  fprodntriv  15898  prodss  15903  fprodss  15904  binomfallfac  15997  bpoly1  16007  bpoly2  16013  bpoly3  16014  ruclem6  16193  smupf  16438  gcdcl  16466  lcmcl  16561  lcmfcl  16588  2mulprm  16653  pcxnn0cl  16822  pcxcl  16823  pcmptcl  16853  infpnlem2  16873  zgz  16895  4sqlem2  16911  4sqlem19  16925  vdwapval  16935  hashbc0  16967  ramcl2  16978  0ramcl  16985  ramcl  16991  isstruct2  17110  imasval  17466  imasbas  17467  imasds  17468  imasplusg  17472  imasmulr  17473  imasvsca  17475  imasip  17476  imasle  17478  qusaddvallem  17506  qusaddflem  17507  qusaddval  17508  qusaddf  17509  qusmulval  17510  qusmulf  17511  mreexexlem3d  17603  sscpwex  17773  fullresc  17809  estrres  18096  evlfcl  18179  ipopos  18493  gsumress  18641  submnd0  18722  qusgrp2  19025  mulgfval  19036  issubg2  19108  triv1nsgd  19139  0subgALT  19534  torsubg  19820  frgpnabllem1  19839  lt6abl  19861  ablfaclem3  20055  ablfac2  20057  simpgnsgd  20068  qusrng  20152  srgbinomlem3  20200  ringidss  20249  qusring2  20305  isdrngd  20733  isdrngdOLD  20735  mptscmfsupp0  20913  islss3  20945  ellspsn  20989  lspprel  21081  znf1o  21541  frgpcyg  21563  cnmsgnsubg  21567  phlpropd  21645  cssval  21672  iscss  21673  dsmm0cl  21730  uvcvvcl  21777  m1detdiag  22572  m2detleiblem1  22599  pmatcollpw3fi1lem1  22761  indistopon  22976  indiscld  23066  restbas  23133  ordttopon  23168  iocpnfordt  23190  icomnfordt  23191  lecldbas  23194  fiuncmp  23379  cmpfi  23383  conncompid  23406  dissnlocfin  23504  elpt  23547  xkotop  23563  xkouni  23574  xkohaus  23628  xkoptsub  23629  imastopn  23695  filconn  23858  cfinufil  23903  alexsublem  24019  alexsub  24020  alexsubALTlem4  24025  distgp  24074  indistgp  24075  ssblps  24397  ssbl  24398  xmeter  24408  nmoi  24703  nmoeq0  24711  0nghm  24716  idnghm  24718  icccld  24741  iocmnfcld  24743  blssioo  24770  xrtgioo  24782  xrsxmet  24785  icccmp  24801  pcopt  24999  pcopt2  25000  elpi1  25022  cmetcaulem  25265  ishl2  25347  rrxmvallem  25381  ovolcl  25455  ovolunlem1a  25473  ovolunnul  25477  ovoliunnul  25484  ioombl1  25539  icombl  25541  ioombl  25542  iccmbl  25543  iccvolcl  25544  ovolioo  25545  ioovolcl  25547  ioorcl  25554  uniioovol  25556  uniioombllem2a  25559  uniioombllem4  25563  uniioombllem5  25564  vitalilem1  25585  vitalilem5  25589  mbfconstlem  25604  mbfima  25607  mbfid  25612  ismbf2d  25617  mbfss  25623  mbfmulc2lem  25624  i1fd  25658  itg1addlem2  25674  itg1addlem4  25676  itg1addlem5  25677  i1fmulc  25680  itg2l  25706  itg2cl  25709  ibl0  25764  iblrelem  25768  iblpos  25770  iblss2  25783  bddmulibl  25816  bddiblnc  25819  recnperf  25882  ply1remlem  26140  fta1glem1  26143  fta1g  26145  elply  26170  plypf1  26187  coefv0  26223  coemulc  26230  fta1  26285  elqaalem2  26297  aannenlem2  26306  aalioulem3  26311  taylfvallem1  26333  tayl0  26338  ulm0  26369  logtayl  26637  atanrecl  26888  atanbnd  26903  harmonicbnd3  26985  ftalem7  27056  basellem5  27062  ppifi  27083  sqff1o  27159  1sgmprm  27176  logexprlim  27202  dchrelbasd  27216  dchr1re  27240  lgslem4  27277  lgsne0  27312  2sqlem9  27404  2sqlem10  27405  rpvmasumlem  27464  dchrisumlem1  27466  vmalogdivsum  27516  pntrlog2bndlem5  27558  ostth  27616  lrrecse  27948  sltmuls1  28153  sltmuls2  28154  mulsuniflem  28155  noseqex  28295  n0mulscl  28351  n0fincut  28361  eln0s  28367  n0subs  28369  n0zs  28395  expscllem  28436  elz12s  28478  tgcgr4  28613  axlowdimlem16  29040  fusgrfisbase  29411  vtxdg0e  29558  rgrusgrprc  29673  wwlksnfi  29989  trlsegvdeglem7  30311  eulerpathpr  30325  0blo  30878  nmlno0lem  30879  omlsilem  31488  pjoc1i  31517  nonbooli  31737  nmlnop0iALT  32081  unopbd  32101  leoprf2  32213  opsqrlem4  32229  opsqrlem5  32230  pjbdlni  32235  pjcmul1i  32287  mptiffisupp  32781  sgncl  32919  drngidlhash  33509  evl1deg1  33651  ply1dg1rt  33655  ply1dg3rt0irred  33659  m1pmeq  33660  mplmulmvr  33698  esplyfvaln  33733  vieta  33739  lvecendof1f1o  33793  fldext2rspun  33842  constrabscl  33938  zarcmplem  34041  prsssdm  34077  ordtrestNEW  34081  esumpad  34215  esumpad2  34216  esumcst  34223  esumrnmpt2  34228  sibf0  34494  sitgclcn  34504  sitgclre  34505  eulerpartlemgs2  34540  dstfrvclim1  34638  ballotlemfelz  34651  signstfveq0  34737  breprexp  34793  r1wf  35255  fineqvnttrclselem1  35281  wevgblacfn  35307  subfacp1lem3  35380  rellysconn  35449  cvmlift2lem9  35509  nnuni  35925  ordcmp  36645  bj-snex  37358  finxpreclem4  37724  poimirlem16  37971  poimirlem17  37972  voliunnfl  37999  mbfresfi  38001  itg2addnclem2  38007  dvasin  38039  heiborlem4  38149  heiborlem6  38151  itrere  42764  sn-itrere  42947  sn-retire  42948  wepwsolem  43488  flcidc  43616  iocmbl  43659  arearect  43661  omcl3g  43780  iscard4  43978  briunov2uz  44143  eliunov2uz  44144  frege124d  44206  frege129d  44208  frege92  44400  lhe4.4ex1a  44774  dvconstbi  44779  binomcxplemnn0  44794  binomcxplemnotnn0  44801  infxr  45814  infleinflem2  45818  climneg  46058  cncfiooicc  46340  itgsinexplem1  46400  volioof  46433  stoweidlem36  46482  wallispilem3  46513  fourierdlem93  46645  fouriersw  46677  fouriercn  46678  etransclem16  46696  etransclem33  46713  sge0reuz  46893  nnfoctbdjlem  46901  hoidmvlelem3  47043  sinnpoly  47351  dfatafv2ex  47673  sprsymrelfvlem  47962  fmtnofz04prm  48052  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  gpg3nbgrvtx0  48564  lincext2  48943  blennn0elnn  49065  itcovalsucov  49156  resccat  49561  funcf2lem2  49569  isnatd  49710  swapfelvv  49750  fucoelvv  49807  prcofelvv  49867  termco  49968  prstcprs  50047