Theorem eqeltrdi 2847

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eqeltrrdi  2848  csbexg  5232  unisn2  5234  class2set  5283  snexALT  5312  snexOLD  5371  prexOLD  5372  iotaex  6461  fvrn0  6855  f0cli  7039  funsneqopb  7095  fmptsng  7112  fmptsnd  7113  elimdelov  7452  ovima0  7535  ndmovcl  7541  caovmo  7593  soex  7861  zfrep6OLD  7897  1st2ndb  7971  fprresex  8250  smofvon2  8286  tz7.44-2  8336  oesuclem  8450  omcl  8461  oecl  8462  nnmcl  8538  nnecl  8539  fsetex  8793  fsetexb  8801  ixpexg  8860  resixpfo  8874  xpsnen  8989  ssfi  9097  cnvfi  9100  nnunifi  9191  imafiOLD  9216  prfi  9224  fsuppun  9290  0fsupp  9293  oiexg  9440  hartogslem1  9447  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  20737  isdrngdOLD  20739  mptscmfsupp0  20917  islss3  20949  ellspsn  20993  lspprel  21084  znf1o  21526  frgpcyg  21548  cnmsgnsubg  21552  phlpropd  21630  cssval  21657  iscss  21658  dsmm0cl  21715  uvcvvcl  21762  m1detdiag  22580  m2detleiblem1  22607  pmatcollpw3fi1lem1  22769  indistopon  22984  indiscld  23074  restbas  23141  ordttopon  23176  iocpnfordt  23198  icomnfordt  23199  lecldbas  23202  fiuncmp  23387  cmpfi  23391  conncompid  23414  dissnlocfin  23512  elpt  23555  xkotop  23571  xkouni  23582  xkohaus  23636  xkoptsub  23637  imastopn  23703  filconn  23866  cfinufil  23911  alexsublem  24027  alexsub  24028  alexsubALTlem4  24033  distgp  24082  indistgp  24083  ssblps  24405  ssbl  24406  xmeter  24416  nmoi  24711  nmoeq0  24719  0nghm  24724  idnghm  24726  icccld  24749  iocmnfcld  24751  blssioo  24778  xrtgioo  24790  xrsxmet  24793  icccmp  24809  pcopt  25007  pcopt2  25008  elpi1  25030  cmetcaulem  25273  ishl2  25355  rrxmvallem  25389  ovolcl  25463  ovolunlem1a  25481  ovolunnul  25485  ovoliunnul  25492  ioombl1  25547  icombl  25549  ioombl  25550  iccmbl  25551  iccvolcl  25552  ovolioo  25553  ioovolcl  25555  ioorcl  25562  uniioovol  25564  uniioombllem2a  25567  uniioombllem4  25571  uniioombllem5  25572  vitalilem1  25593  vitalilem5  25597  mbfconstlem  25612  mbfima  25615  mbfid  25620  ismbf2d  25625  mbfss  25631  mbfmulc2lem  25632  i1fd  25666  itg1addlem2  25682  itg1addlem4  25684  itg1addlem5  25685  i1fmulc  25688  itg2l  25714  itg2cl  25717  ibl0  25772  iblrelem  25776  iblpos  25778  iblss2  25791  bddmulibl  25824  bddiblnc  25827  recnperf  25890  ply1remlem  26148  fta1glem1  26151  fta1g  26153  elply  26178  plypf1  26195  coefv0  26231  coemulc  26238  fta1  26292  elqaalem2  26304  aannenlem2  26313  aalioulem3  26318  taylfvallem1  26340  tayl0  26345  ulm0  26374  logtayl  26642  atanrecl  26893  atanbnd  26908  harmonicbnd3  26989  ftalem7  27060  basellem5  27066  ppifi  27087  sqff1o  27163  1sgmprm  27180  logexprlim  27206  dchrelbasd  27220  dchr1re  27244  lgslem4  27281  lgsne0  27316  2sqlem9  27408  2sqlem10  27409  rpvmasumlem  27468  dchrisumlem1  27470  vmalogdivsum  27520  pntrlog2bndlem5  27562  ostth  27620  lrrecse  27952  sltmuls1  28157  sltmuls2  28158  mulsuniflem  28159  noseqex  28299  n0mulscl  28355  n0fincut  28365  eln0s  28371  n0subs  28373  n0zs  28399  expscllem  28440  elz12s  28482  tgcgr4  28617  axlowdimlem16  29044  fusgrfisbase  29415  vtxdg0e  29561  rgrusgrprc  29676  wwlksnfi  29992  trlsegvdeglem7  30314  eulerpathpr  30328  0blo  30881  nmlno0lem  30882  omlsilem  31491  pjoc1i  31520  nonbooli  31740  nmlnop0iALT  32084  unopbd  32104  leoprf2  32216  opsqrlem4  32232  opsqrlem5  32233  pjbdlni  32238  pjcmul1i  32290  mptiffisupp  32785  sgncl  32923  drngidlhash  33517  evl1deg1  33659  ply1dg1rt  33663  ply1dg3rt0irred  33667  m1pmeq  33668  mplmulmvr  33723  esplyfvaln  33758  vieta  33764  lvecendof1f1o  33817  fldext2rspun  33866  constrabscl  33962  zarcmplem  34065  prsssdm  34101  ordtrestNEW  34105  esumpad  34239  esumpad2  34240  esumcst  34247  esumrnmpt2  34252  sibf0  34518  sitgclcn  34528  sitgclre  34529  eulerpartlemgs2  34564  dstfrvclim1  34662  ballotlemfelz  34675  signstfveq0  34761  breprexp  34817  r1wf  35277  fineqvnttrclselem1  35302  wevgblacfn  35337  subfacp1lem3  35410  rellysconn  35479  cvmlift2lem9  35539  nnuni  35955  ordcmp  36675  bj-snex  37388  finxpreclem4  37756  poimirlem16  38003  poimirlem17  38004  voliunnfl  38031  mbfresfi  38033  itg2addnclem2  38039  dvasin  38071  heiborlem4  38181  heiborlem6  38183  itrere  42795  sn-itrere  42978  sn-retire  42979  wepwsolem  43487  flcidc  43615  iocmbl  43658  arearect  43660  omcl3g  43779  iscard4  43977  briunov2uz  44142  eliunov2uz  44143  frege124d  44205  frege129d  44207  frege92  44399  lhe4.4ex1a  44773  dvconstbi  44778  binomcxplemnn0  44793  binomcxplemnotnn0  44800  infxr  45811  infleinflem2  45815  climneg  46055  cncfiooicc  46337  itgsinexplem1  46397  volioof  46430  stoweidlem36  46479  wallispilem3  46510  fourierdlem93  46642  fouriersw  46674  fouriercn  46675  etransclem16  46693  etransclem33  46710  sge0reuz  46890  nnfoctbdjlem  46898  hoidmvlelem3  47040  sinnpoly  47354  dfatafv2ex  47676  sprsymrelfvlem  47965  fmtnofz04prm  48055  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  gpg3nbgrvtx0  48567  lincext2  48946  blennn0elnn  49068  itcovalsucov  49159  resccat  49564  funcf2lem2  49572  isnatd  49713  swapfelvv  49753  fucoelvv  49810  prcofelvv  49870  termco  49971  prstcprs  50050