Theorem eqeltrdi 2849

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqeltrrdi  2850  csbexg  5310  unisn2  5312  class2set  5355  snexALT  5383  snex  5436  prex  5437  iotaex  6534  iotaexOLD  6541  fvrn0  6936  f0cli  7118  funsneqopb  7172  fmptsng  7188  fmptsnd  7189  elimdelov  7529  ovima0  7612  ndmovcl  7618  caovmo  7670  soex  7943  zfrep6  7979  1st2ndb  8054  fprresex  8335  wfrlem17OLD  8365  smofvon2  8396  tz7.44-2  8447  oesuclem  8563  omcl  8574  oecl  8575  nnmcl  8650  nnecl  8651  fsetex  8896  fsetexb  8904  ixpexg  8962  resixpfo  8976  xpsnen  9095  ssfi  9213  cnvfi  9216  nnunifi  9327  imafiOLD  9354  xpfiOLD  9359  prfi  9363  fsuppun  9427  0fsupp  9430  oiexg  9575  hartogslem1  9582  cantnfvalf  9705  rnttrcl  9762  ttrclse  9767  rankdmr1  9841  rankr1c  9861  numwdom  10099  alephon  10109  isfin5  10339  sdom2en01  10342  isf32lem9  10401  hsmexlem9  10465  iundom2g  10580  gchxpidm  10709  r1tskina  10822  tskmcl  10881  recmulnq  11004  recclnq  11006  genpelv  11040  un0mulcl  12560  znegcl  12652  zeo  12704  eqreznegel  12976  xnegcl  13255  xnn0xaddcl  13277  ioorebas  13491  modid0  13937  2txmodxeq0  13972  fzofi  14015  seqexw  14058  expcllem  14113  m1expcl2  14126  faclbnd4lem3  14334  bccl  14361  hasheq0  14402  hashrabrsn  14411  fnfz0hashnn0  14487  fnfzo0hashnn0  14490  wrdnfi  14586  cshwcl  14836  relexpaddg  15092  abs00bd  15330  iserge0  15697  sumrblem  15747  fsumcvg  15748  summolem2a  15751  sumss  15760  fsumss  15761  fsumcvg2  15763  sumsplit  15804  binom  15866  bcxmas  15871  geomulcvg  15912  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  fprodntriv  15978  prodss  15983  fprodss  15984  binomfallfac  16077  bpoly1  16087  bpoly2  16093  bpoly3  16094  ruclem6  16271  smupf  16515  gcdcl  16543  lcmcl  16638  lcmfcl  16665  2mulprm  16730  pcxnn0cl  16898  pcxcl  16899  pcmptcl  16929  infpnlem2  16949  zgz  16971  4sqlem2  16987  4sqlem19  17001  vdwapval  17011  hashbc0  17043  ramcl2  17054  0ramcl  17061  ramcl  17067  isstruct2  17186  imasval  17556  imasbas  17557  imasds  17558  imasplusg  17562  imasmulr  17563  imasvsca  17565  imasip  17566  imasle  17568  qusaddvallem  17596  qusaddflem  17597  qusaddval  17598  qusaddf  17599  qusmulval  17600  qusmulf  17601  mreexexlem3d  17689  sscpwex  17859  fullresc  17896  estrres  18184  evlfcl  18267  ipopos  18581  gsumress  18695  submnd0  18776  qusgrp2  19076  mulgfval  19087  issubg2  19159  triv1nsgd  19191  0subgALT  19586  torsubg  19872  frgpnabllem1  19891  lt6abl  19913  ablfaclem3  20107  ablfac2  20109  simpgnsgd  20120  qusrng  20177  srgbinomlem3  20225  ringidss  20274  qusring2  20331  isdrngd  20765  isdrngdOLD  20767  mptscmfsupp0  20925  islss3  20957  ellspsn  21001  lspprel  21093  znf1o  21570  frgpcyg  21592  cnmsgnsubg  21595  phlpropd  21673  cssval  21700  iscss  21701  dsmm0cl  21760  uvcvvcl  21807  m1detdiag  22603  m2detleiblem1  22630  pmatcollpw3fi1lem1  22792  indistopon  23008  indiscld  23099  restbas  23166  ordttopon  23201  iocpnfordt  23223  icomnfordt  23224  lecldbas  23227  fiuncmp  23412  cmpfi  23416  conncompid  23439  dissnlocfin  23537  elpt  23580  xkotop  23596  xkouni  23607  xkohaus  23661  xkoptsub  23662  imastopn  23728  filconn  23891  cfinufil  23936  alexsublem  24052  alexsub  24053  alexsubALTlem4  24058  distgp  24107  indistgp  24108  ssblps  24432  ssbl  24433  xmeter  24443  nmoi  24749  nmoeq0  24757  0nghm  24762  idnghm  24764  icccld  24787  iocmnfcld  24789  blssioo  24816  xrtgioo  24828  xrsxmet  24831  icccmp  24847  pcopt  25055  pcopt2  25056  elpi1  25078  cmetcaulem  25322  ishl2  25404  rrxmvallem  25438  ovolcl  25513  ovolunlem1a  25531  ovolunnul  25535  ovoliunnul  25542  ioombl1  25597  icombl  25599  ioombl  25600  iccmbl  25601  iccvolcl  25602  ovolioo  25603  ioovolcl  25605  ioorcl  25612  uniioovol  25614  uniioombllem2a  25617  uniioombllem4  25621  uniioombllem5  25622  vitalilem1  25643  vitalilem5  25647  mbfconstlem  25662  mbfima  25665  mbfid  25670  ismbf2d  25675  mbfss  25681  mbfmulc2lem  25682  i1fd  25716  itg1addlem2  25732  itg1addlem4  25734  itg1addlem5  25735  i1fmulc  25738  itg2l  25764  itg2cl  25767  ibl0  25822  iblrelem  25826  iblpos  25828  iblss2  25841  bddmulibl  25874  bddiblnc  25877  recnperf  25940  ply1remlem  26204  fta1glem1  26207  fta1g  26209  elply  26234  plypf1  26251  coefv0  26287  coemulc  26294  fta1  26350  elqaalem2  26362  aannenlem2  26371  aalioulem3  26376  taylfvallem1  26398  tayl0  26403  ulm0  26434  logtayl  26702  atanrecl  26954  atanbnd  26969  harmonicbnd3  27051  ftalem7  27122  basellem5  27128  ppifi  27149  sqff1o  27225  1sgmprm  27243  logexprlim  27269  dchrelbasd  27283  dchr1re  27307  lgslem4  27344  lgsne0  27379  2sqlem9  27471  2sqlem10  27472  rpvmasumlem  27531  dchrisumlem1  27533  vmalogdivsum  27583  pntrlog2bndlem5  27625  ostth  27683  lrrecse  27975  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  noseqex  28295  n0mulscl  28348  eln0s  28358  n0subs  28360  n0zs  28375  expscl  28413  elzs12  28421  tgcgr4  28539  axlowdimlem16  28972  fusgrfisbase  29345  vtxdg0e  29492  rgrusgrprc  29607  wwlksnfi  29926  trlsegvdeglem7  30245  eulerpathpr  30259  0blo  30811  nmlno0lem  30812  omlsilem  31421  pjoc1i  31450  nonbooli  31670  nmlnop0iALT  32014  unopbd  32034  leoprf2  32146  opsqrlem4  32162  opsqrlem5  32163  pjbdlni  32168  pjcmul1i  32220  mptiffisupp  32702  drngidlhash  33462  evl1deg1  33601  ply1dg1rt  33604  ply1dg3rt0irred  33607  m1pmeq  33608  lvecendof1f1o  33684  fldext2rspun  33732  zarcmplem  33880  prsssdm  33916  ordtrestNEW  33920  esumpad  34056  esumpad2  34057  esumcst  34064  esumrnmpt2  34069  sibf0  34336  sitgclcn  34346  sitgclre  34347  eulerpartlemgs2  34382  dstfrvclim1  34480  ballotlemfelz  34493  sgncl  34541  signstfveq0  34592  breprexp  34648  wevgblacfn  35114  subfacp1lem3  35187  rellysconn  35256  cvmlift2lem9  35316  nnuni  35727  ordcmp  36448  bj-snex  37036  finxpreclem4  37395  poimirlem16  37643  poimirlem17  37644  voliunnfl  37671  mbfresfi  37673  itg2addnclem2  37679  dvasin  37711  heiborlem4  37821  heiborlem6  37823  itrere  42353  sn-itrere  42498  sn-retire  42499  wepwsolem  43054  flcidc  43182  iocmbl  43225  arearect  43227  omcl3g  43347  iscard4  43546  briunov2uz  43711  eliunov2uz  43712  frege124d  43774  frege129d  43776  frege92  43968  lhe4.4ex1a  44348  dvconstbi  44353  binomcxplemnn0  44368  binomcxplemnotnn0  44375  infxr  45378  infleinflem2  45382  climneg  45625  cncfiooicc  45909  itgsinexplem1  45969  volioof  46002  stoweidlem36  46051  wallispilem3  46082  fourierdlem93  46214  fouriersw  46246  fouriercn  46247  etransclem16  46265  etransclem33  46282  sge0reuz  46462  nnfoctbdjlem  46470  hoidmvlelem3  46612  upwordnul  46895  dfatafv2ex  47225  sprsymrelfvlem  47477  fmtnofz04prm  47564  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  gpg3nbgrvtx0  48032  lincext2  48372  blennn0elnn  48498  itcovalsucov  48589  funcf2lem2  48915  isnatd  48949  swapfelvv  48969  fucoelvv  49015  prstcprs  49164