Theorem eqeltrdi 2844

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqeltrrdi  2845  csbexg  5255  unisn2  5257  class2set  5300  snexALT  5328  snex  5381  prex  5382  iotaex  6468  fvrn0  6862  f0cli  7043  funsneqopb  7097  fmptsng  7114  fmptsnd  7115  elimdelov  7454  ovima0  7537  ndmovcl  7543  caovmo  7595  soex  7863  zfrep6  7899  1st2ndb  7973  fprresex  8252  smofvon2  8288  tz7.44-2  8338  oesuclem  8452  omcl  8463  oecl  8464  nnmcl  8540  nnecl  8541  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  9574  rnttrcl  9631  ttrclse  9636  rankdmr1  9713  rankr1c  9733  numwdom  9969  alephon  9979  isfin5  10209  sdom2en01  10212  isf32lem9  10271  hsmexlem9  10335  iundom2g  10450  gchxpidm  10580  r1tskina  10693  tskmcl  10752  recmulnq  10875  recclnq  10877  genpelv  10911  un0mulcl  12435  znegcl  12526  zeo  12578  eqreznegel  12847  xnegcl  13128  xnn0xaddcl  13150  ioorebas  13367  modid0  13817  2txmodxeq0  13854  fzofi  13897  seqexw  13940  expcllem  13995  m1expcl2  14008  faclbnd4lem3  14218  bccl  14245  hasheq0  14286  hashrabrsn  14295  fnfz0hashnn0  14371  fnfzo0hashnn0  14374  wrdnfi  14471  cshwcl  14721  relexpaddg  14976  abs00bd  15214  iserge0  15584  sumrblem  15634  fsumcvg  15635  summolem2a  15638  sumss  15647  fsumss  15648  fsumcvg2  15650  sumsplit  15691  binom  15753  bcxmas  15758  geomulcvg  15799  prodrblem  15852  fprodcvg  15853  prodmolem2a  15857  zprod  15860  fprodntriv  15865  prodss  15870  fprodss  15871  binomfallfac  15964  bpoly1  15974  bpoly2  15980  bpoly3  15981  ruclem6  16160  smupf  16405  gcdcl  16433  lcmcl  16528  lcmfcl  16555  2mulprm  16620  pcxnn0cl  16788  pcxcl  16789  pcmptcl  16819  infpnlem2  16839  zgz  16861  4sqlem2  16877  4sqlem19  16891  vdwapval  16901  hashbc0  16933  ramcl2  16944  0ramcl  16951  ramcl  16957  isstruct2  17076  imasval  17432  imasbas  17433  imasds  17434  imasplusg  17438  imasmulr  17439  imasvsca  17441  imasip  17442  imasle  17444  qusaddvallem  17472  qusaddflem  17473  qusaddval  17474  qusaddf  17475  qusmulval  17476  qusmulf  17477  mreexexlem3d  17569  sscpwex  17739  fullresc  17775  estrres  18062  evlfcl  18145  ipopos  18459  gsumress  18607  submnd0  18688  qusgrp2  18988  mulgfval  18999  issubg2  19071  triv1nsgd  19102  0subgALT  19497  torsubg  19783  frgpnabllem1  19802  lt6abl  19824  ablfaclem3  20018  ablfac2  20020  simpgnsgd  20031  qusrng  20115  srgbinomlem3  20163  ringidss  20212  qusring2  20270  isdrngd  20698  isdrngdOLD  20700  mptscmfsupp0  20878  islss3  20910  ellspsn  20954  lspprel  21046  znf1o  21506  frgpcyg  21528  cnmsgnsubg  21532  phlpropd  21610  cssval  21637  iscss  21638  dsmm0cl  21695  uvcvvcl  21742  m1detdiag  22541  m2detleiblem1  22568  pmatcollpw3fi1lem1  22730  indistopon  22945  indiscld  23035  restbas  23102  ordttopon  23137  iocpnfordt  23159  icomnfordt  23160  lecldbas  23163  fiuncmp  23348  cmpfi  23352  conncompid  23375  dissnlocfin  23473  elpt  23516  xkotop  23532  xkouni  23543  xkohaus  23597  xkoptsub  23598  imastopn  23664  filconn  23827  cfinufil  23872  alexsublem  23988  alexsub  23989  alexsubALTlem4  23994  distgp  24043  indistgp  24044  ssblps  24366  ssbl  24367  xmeter  24377  nmoi  24672  nmoeq0  24680  0nghm  24685  idnghm  24687  icccld  24710  iocmnfcld  24712  blssioo  24739  xrtgioo  24751  xrsxmet  24754  icccmp  24770  pcopt  24978  pcopt2  24979  elpi1  25001  cmetcaulem  25244  ishl2  25326  rrxmvallem  25360  ovolcl  25435  ovolunlem1a  25453  ovolunnul  25457  ovoliunnul  25464  ioombl1  25519  icombl  25521  ioombl  25522  iccmbl  25523  iccvolcl  25524  ovolioo  25525  ioovolcl  25527  ioorcl  25534  uniioovol  25536  uniioombllem2a  25539  uniioombllem4  25543  uniioombllem5  25544  vitalilem1  25565  vitalilem5  25569  mbfconstlem  25584  mbfima  25587  mbfid  25592  ismbf2d  25597  mbfss  25603  mbfmulc2lem  25604  i1fd  25638  itg1addlem2  25654  itg1addlem4  25656  itg1addlem5  25657  i1fmulc  25660  itg2l  25686  itg2cl  25689  ibl0  25744  iblrelem  25748  iblpos  25750  iblss2  25763  bddmulibl  25796  bddiblnc  25799  recnperf  25862  ply1remlem  26126  fta1glem1  26129  fta1g  26131  elply  26156  plypf1  26173  coefv0  26209  coemulc  26216  fta1  26272  elqaalem2  26284  aannenlem2  26293  aalioulem3  26298  taylfvallem1  26320  tayl0  26325  ulm0  26356  logtayl  26625  atanrecl  26877  atanbnd  26892  harmonicbnd3  26974  ftalem7  27045  basellem5  27051  ppifi  27072  sqff1o  27148  1sgmprm  27166  logexprlim  27192  dchrelbasd  27206  dchr1re  27230  lgslem4  27267  lgsne0  27302  2sqlem9  27394  2sqlem10  27395  rpvmasumlem  27454  dchrisumlem1  27456  vmalogdivsum  27506  pntrlog2bndlem5  27548  ostth  27606  lrrecse  27938  sltmuls1  28143  sltmuls2  28144  mulsuniflem  28145  noseqex  28285  n0mulscl  28341  n0fincut  28351  eln0s  28357  n0subs  28359  n0zs  28385  expscllem  28426  elz12s  28468  tgcgr4  28603  axlowdimlem16  29030  fusgrfisbase  29401  vtxdg0e  29548  rgrusgrprc  29663  wwlksnfi  29979  trlsegvdeglem7  30301  eulerpathpr  30315  0blo  30867  nmlno0lem  30868  omlsilem  31477  pjoc1i  31506  nonbooli  31726  nmlnop0iALT  32070  unopbd  32090  leoprf2  32202  opsqrlem4  32218  opsqrlem5  32219  pjbdlni  32224  pjcmul1i  32276  mptiffisupp  32772  sgncl  32912  drngidlhash  33515  evl1deg1  33657  ply1dg1rt  33661  ply1dg3rt0irred  33665  m1pmeq  33666  mplmulmvr  33704  vieta  33736  lvecendof1f1o  33790  fldext2rspun  33839  constrabscl  33935  zarcmplem  34038  prsssdm  34074  ordtrestNEW  34078  esumpad  34212  esumpad2  34213  esumcst  34220  esumrnmpt2  34225  sibf0  34491  sitgclcn  34501  sitgclre  34502  eulerpartlemgs2  34537  dstfrvclim1  34635  ballotlemfelz  34648  signstfveq0  34734  breprexp  34790  r1wf  35252  fineqvnttrclselem1  35277  wevgblacfn  35303  subfacp1lem3  35376  rellysconn  35445  cvmlift2lem9  35505  nnuni  35921  ordcmp  36641  bj-snex  37236  finxpreclem4  37599  poimirlem16  37837  poimirlem17  37838  voliunnfl  37865  mbfresfi  37867  itg2addnclem2  37873  dvasin  37905  heiborlem4  38015  heiborlem6  38017  itrere  42573  sn-itrere  42743  sn-retire  42744  wepwsolem  43284  flcidc  43412  iocmbl  43455  arearect  43457  omcl3g  43576  iscard4  43774  briunov2uz  43939  eliunov2uz  43940  frege124d  44002  frege129d  44004  frege92  44196  lhe4.4ex1a  44570  dvconstbi  44575  binomcxplemnn0  44590  binomcxplemnotnn0  44597  infxr  45611  infleinflem2  45615  climneg  45856  cncfiooicc  46138  itgsinexplem1  46198  volioof  46231  stoweidlem36  46280  wallispilem3  46311  fourierdlem93  46443  fouriersw  46475  fouriercn  46476  etransclem16  46494  etransclem33  46511  sge0reuz  46691  nnfoctbdjlem  46699  hoidmvlelem3  46841  sinnpoly  47137  dfatafv2ex  47459  sprsymrelfvlem  47736  fmtnofz04prm  47823  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  gpg3nbgrvtx0  48322  lincext2  48701  blennn0elnn  48823  itcovalsucov  48914  resccat  49319  funcf2lem2  49327  isnatd  49468  swapfelvv  49508  fucoelvv  49565  prcofelvv  49625  termco  49726  prstcprs  49805