Theorem eqeltrdi 2836

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqeltrrdi  2837  csbexg  5265  unisn2  5267  class2set  5310  snexALT  5338  snex  5391  prex  5392  iotaex  6484  iotaexOLD  6491  fvrn0  6888  f0cli  7070  funsneqopb  7124  fmptsng  7142  fmptsnd  7143  elimdelov  7485  ovima0  7568  ndmovcl  7574  caovmo  7626  soex  7897  zfrep6  7933  1st2ndb  8008  fprresex  8289  smofvon2  8325  tz7.44-2  8375  oesuclem  8489  omcl  8500  oecl  8501  nnmcl  8576  nnecl  8577  fsetex  8829  fsetexb  8837  ixpexg  8895  resixpfo  8909  xpsnen  9025  ssfi  9137  cnvfi  9140  nnunifi  9238  imafiOLD  9265  xpfiOLD  9270  prfi  9274  fsuppun  9338  0fsupp  9341  oiexg  9488  hartogslem1  9495  cantnfvalf  9618  rnttrcl  9675  ttrclse  9680  rankdmr1  9754  rankr1c  9774  numwdom  10012  alephon  10022  isfin5  10252  sdom2en01  10255  isf32lem9  10314  hsmexlem9  10378  iundom2g  10493  gchxpidm  10622  r1tskina  10735  tskmcl  10794  recmulnq  10917  recclnq  10919  genpelv  10953  un0mulcl  12476  znegcl  12568  zeo  12620  eqreznegel  12893  xnegcl  13173  xnn0xaddcl  13195  ioorebas  13412  modid0  13859  2txmodxeq0  13896  fzofi  13939  seqexw  13982  expcllem  14037  m1expcl2  14050  faclbnd4lem3  14260  bccl  14287  hasheq0  14328  hashrabrsn  14337  fnfz0hashnn0  14413  fnfzo0hashnn0  14416  wrdnfi  14513  cshwcl  14763  relexpaddg  15019  abs00bd  15257  iserge0  15627  sumrblem  15677  fsumcvg  15678  summolem2a  15681  sumss  15690  fsumss  15691  fsumcvg2  15693  sumsplit  15734  binom  15796  bcxmas  15801  geomulcvg  15842  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  fprodntriv  15908  prodss  15913  fprodss  15914  binomfallfac  16007  bpoly1  16017  bpoly2  16023  bpoly3  16024  ruclem6  16203  smupf  16448  gcdcl  16476  lcmcl  16571  lcmfcl  16598  2mulprm  16663  pcxnn0cl  16831  pcxcl  16832  pcmptcl  16862  infpnlem2  16882  zgz  16904  4sqlem2  16920  4sqlem19  16934  vdwapval  16944  hashbc0  16976  ramcl2  16987  0ramcl  16994  ramcl  17000  isstruct2  17119  imasval  17474  imasbas  17475  imasds  17476  imasplusg  17480  imasmulr  17481  imasvsca  17483  imasip  17484  imasle  17486  qusaddvallem  17514  qusaddflem  17515  qusaddval  17516  qusaddf  17517  qusmulval  17518  qusmulf  17519  mreexexlem3d  17607  sscpwex  17777  fullresc  17813  estrres  18100  evlfcl  18183  ipopos  18495  gsumress  18609  submnd0  18690  qusgrp2  18990  mulgfval  19001  issubg2  19073  triv1nsgd  19105  0subgALT  19498  torsubg  19784  frgpnabllem1  19803  lt6abl  19825  ablfaclem3  20019  ablfac2  20021  simpgnsgd  20032  qusrng  20089  srgbinomlem3  20137  ringidss  20186  qusring2  20243  isdrngd  20674  isdrngdOLD  20676  mptscmfsupp0  20833  islss3  20865  ellspsn  20909  lspprel  21001  znf1o  21461  frgpcyg  21483  cnmsgnsubg  21486  phlpropd  21564  cssval  21591  iscss  21592  dsmm0cl  21649  uvcvvcl  21696  m1detdiag  22484  m2detleiblem1  22511  pmatcollpw3fi1lem1  22673  indistopon  22888  indiscld  22978  restbas  23045  ordttopon  23080  iocpnfordt  23102  icomnfordt  23103  lecldbas  23106  fiuncmp  23291  cmpfi  23295  conncompid  23318  dissnlocfin  23416  elpt  23459  xkotop  23475  xkouni  23486  xkohaus  23540  xkoptsub  23541  imastopn  23607  filconn  23770  cfinufil  23815  alexsublem  23931  alexsub  23932  alexsubALTlem4  23937  distgp  23986  indistgp  23987  ssblps  24310  ssbl  24311  xmeter  24321  nmoi  24616  nmoeq0  24624  0nghm  24629  idnghm  24631  icccld  24654  iocmnfcld  24656  blssioo  24683  xrtgioo  24695  xrsxmet  24698  icccmp  24714  pcopt  24922  pcopt2  24923  elpi1  24945  cmetcaulem  25188  ishl2  25270  rrxmvallem  25304  ovolcl  25379  ovolunlem1a  25397  ovolunnul  25401  ovoliunnul  25408  ioombl1  25463  icombl  25465  ioombl  25466  iccmbl  25467  iccvolcl  25468  ovolioo  25469  ioovolcl  25471  ioorcl  25478  uniioovol  25480  uniioombllem2a  25483  uniioombllem4  25487  uniioombllem5  25488  vitalilem1  25509  vitalilem5  25513  mbfconstlem  25528  mbfima  25531  mbfid  25536  ismbf2d  25541  mbfss  25547  mbfmulc2lem  25548  i1fd  25582  itg1addlem2  25598  itg1addlem4  25600  itg1addlem5  25601  i1fmulc  25604  itg2l  25630  itg2cl  25633  ibl0  25688  iblrelem  25692  iblpos  25694  iblss2  25707  bddmulibl  25740  bddiblnc  25743  recnperf  25806  ply1remlem  26070  fta1glem1  26073  fta1g  26075  elply  26100  plypf1  26117  coefv0  26153  coemulc  26160  fta1  26216  elqaalem2  26228  aannenlem2  26237  aalioulem3  26242  taylfvallem1  26264  tayl0  26269  ulm0  26300  logtayl  26569  atanrecl  26821  atanbnd  26836  harmonicbnd3  26918  ftalem7  26989  basellem5  26995  ppifi  27016  sqff1o  27092  1sgmprm  27110  logexprlim  27136  dchrelbasd  27150  dchr1re  27174  lgslem4  27211  lgsne0  27246  2sqlem9  27338  2sqlem10  27339  rpvmasumlem  27398  dchrisumlem1  27400  vmalogdivsum  27450  pntrlog2bndlem5  27492  ostth  27550  lrrecse  27849  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  noseqex  28183  n0mulscl  28237  n0sfincut  28246  eln0s  28251  n0subs  28253  n0zs  28277  expscllem  28316  elzs12  28337  tgcgr4  28458  axlowdimlem16  28884  fusgrfisbase  29255  vtxdg0e  29402  rgrusgrprc  29517  wwlksnfi  29836  trlsegvdeglem7  30155  eulerpathpr  30169  0blo  30721  nmlno0lem  30722  omlsilem  31331  pjoc1i  31360  nonbooli  31580  nmlnop0iALT  31924  unopbd  31944  leoprf2  32056  opsqrlem4  32072  opsqrlem5  32073  pjbdlni  32078  pjcmul1i  32130  mptiffisupp  32616  sgncl  32756  drngidlhash  33405  evl1deg1  33545  ply1dg1rt  33548  ply1dg3rt0irred  33551  m1pmeq  33552  lvecendof1f1o  33629  fldext2rspun  33677  constrabscl  33768  zarcmplem  33871  prsssdm  33907  ordtrestNEW  33911  esumpad  34045  esumpad2  34046  esumcst  34053  esumrnmpt2  34058  sibf0  34325  sitgclcn  34335  sitgclre  34336  eulerpartlemgs2  34371  dstfrvclim1  34469  ballotlemfelz  34482  signstfveq0  34568  breprexp  34624  wevgblacfn  35096  subfacp1lem3  35169  rellysconn  35238  cvmlift2lem9  35298  nnuni  35714  ordcmp  36435  bj-snex  37023  finxpreclem4  37382  poimirlem16  37630  poimirlem17  37631  voliunnfl  37658  mbfresfi  37660  itg2addnclem2  37666  dvasin  37698  heiborlem4  37808  heiborlem6  37810  itrere  42306  sn-itrere  42476  sn-retire  42477  wepwsolem  43031  flcidc  43159  iocmbl  43202  arearect  43204  omcl3g  43323  iscard4  43522  briunov2uz  43687  eliunov2uz  43688  frege124d  43750  frege129d  43752  frege92  43944  lhe4.4ex1a  44318  dvconstbi  44323  binomcxplemnn0  44338  binomcxplemnotnn0  44345  infxr  45363  infleinflem2  45367  climneg  45608  cncfiooicc  45892  itgsinexplem1  45952  volioof  45985  stoweidlem36  46034  wallispilem3  46065  fourierdlem93  46197  fouriersw  46229  fouriercn  46230  etransclem16  46248  etransclem33  46265  sge0reuz  46445  nnfoctbdjlem  46453  hoidmvlelem3  46595  upwordnul  46878  sinnpoly  46892  dfatafv2ex  47214  sprsymrelfvlem  47491  fmtnofz04prm  47578  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  gpg3nbgrvtx0  48067  lincext2  48444  blennn0elnn  48566  itcovalsucov  48657  resccat  49063  funcf2lem2  49071  isnatd  49212  swapfelvv  49252  fucoelvv  49309  prcofelvv  49369  termco  49470  prstcprs  49549