Theorem eqeltrdi 2842

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 2834	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 2707

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

This theorem is referenced by:  eqeltrrdi  2843  csbexg  5280  unisn2  5282  class2set  5325  snexALT  5353  snex  5406  prex  5407  iotaex  6503  iotaexOLD  6510  fvrn0  6905  f0cli  7087  funsneqopb  7141  fmptsng  7159  fmptsnd  7160  elimdelov  7501  ovima0  7584  ndmovcl  7590  caovmo  7642  soex  7915  zfrep6  7951  1st2ndb  8026  fprresex  8307  wfrlem17OLD  8337  smofvon2  8368  tz7.44-2  8419  oesuclem  8535  omcl  8546  oecl  8547  nnmcl  8622  nnecl  8623  fsetex  8868  fsetexb  8876  ixpexg  8934  resixpfo  8948  xpsnen  9067  ssfi  9185  cnvfi  9188  nnunifi  9297  imafiOLD  9324  xpfiOLD  9329  prfi  9333  fsuppun  9397  0fsupp  9400  oiexg  9547  hartogslem1  9554  cantnfvalf  9677  rnttrcl  9734  ttrclse  9739  rankdmr1  9813  rankr1c  9833  numwdom  10071  alephon  10081  isfin5  10311  sdom2en01  10314  isf32lem9  10373  hsmexlem9  10437  iundom2g  10552  gchxpidm  10681  r1tskina  10794  tskmcl  10853  recmulnq  10976  recclnq  10978  genpelv  11012  un0mulcl  12533  znegcl  12625  zeo  12677  eqreznegel  12948  xnegcl  13227  xnn0xaddcl  13249  ioorebas  13466  modid0  13912  2txmodxeq0  13947  fzofi  13990  seqexw  14033  expcllem  14088  m1expcl2  14101  faclbnd4lem3  14311  bccl  14338  hasheq0  14379  hashrabrsn  14388  fnfz0hashnn0  14464  fnfzo0hashnn0  14467  wrdnfi  14564  cshwcl  14814  relexpaddg  15070  abs00bd  15308  iserge0  15675  sumrblem  15725  fsumcvg  15726  summolem2a  15729  sumss  15738  fsumss  15739  fsumcvg2  15741  sumsplit  15782  binom  15844  bcxmas  15849  geomulcvg  15890  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  zprod  15951  fprodntriv  15956  prodss  15961  fprodss  15962  binomfallfac  16055  bpoly1  16065  bpoly2  16071  bpoly3  16072  ruclem6  16251  smupf  16495  gcdcl  16523  lcmcl  16618  lcmfcl  16645  2mulprm  16710  pcxnn0cl  16878  pcxcl  16879  pcmptcl  16909  infpnlem2  16929  zgz  16951  4sqlem2  16967  4sqlem19  16981  vdwapval  16991  hashbc0  17023  ramcl2  17034  0ramcl  17041  ramcl  17047  isstruct2  17166  imasval  17523  imasbas  17524  imasds  17525  imasplusg  17529  imasmulr  17530  imasvsca  17532  imasip  17533  imasle  17535  qusaddvallem  17563  qusaddflem  17564  qusaddval  17565  qusaddf  17566  qusmulval  17567  qusmulf  17568  mreexexlem3d  17656  sscpwex  17826  fullresc  17862  estrres  18149  evlfcl  18232  ipopos  18544  gsumress  18658  submnd0  18739  qusgrp2  19039  mulgfval  19050  issubg2  19122  triv1nsgd  19154  0subgALT  19547  torsubg  19833  frgpnabllem1  19852  lt6abl  19874  ablfaclem3  20068  ablfac2  20070  simpgnsgd  20081  qusrng  20138  srgbinomlem3  20186  ringidss  20235  qusring2  20292  isdrngd  20723  isdrngdOLD  20725  mptscmfsupp0  20882  islss3  20914  ellspsn  20958  lspprel  21050  znf1o  21510  frgpcyg  21532  cnmsgnsubg  21535  phlpropd  21613  cssval  21640  iscss  21641  dsmm0cl  21698  uvcvvcl  21745  m1detdiag  22533  m2detleiblem1  22560  pmatcollpw3fi1lem1  22722  indistopon  22937  indiscld  23027  restbas  23094  ordttopon  23129  iocpnfordt  23151  icomnfordt  23152  lecldbas  23155  fiuncmp  23340  cmpfi  23344  conncompid  23367  dissnlocfin  23465  elpt  23508  xkotop  23524  xkouni  23535  xkohaus  23589  xkoptsub  23590  imastopn  23656  filconn  23819  cfinufil  23864  alexsublem  23980  alexsub  23981  alexsubALTlem4  23986  distgp  24035  indistgp  24036  ssblps  24359  ssbl  24360  xmeter  24370  nmoi  24665  nmoeq0  24673  0nghm  24678  idnghm  24680  icccld  24703  iocmnfcld  24705  blssioo  24732  xrtgioo  24744  xrsxmet  24747  icccmp  24763  pcopt  24971  pcopt2  24972  elpi1  24994  cmetcaulem  25238  ishl2  25320  rrxmvallem  25354  ovolcl  25429  ovolunlem1a  25447  ovolunnul  25451  ovoliunnul  25458  ioombl1  25513  icombl  25515  ioombl  25516  iccmbl  25517  iccvolcl  25518  ovolioo  25519  ioovolcl  25521  ioorcl  25528  uniioovol  25530  uniioombllem2a  25533  uniioombllem4  25537  uniioombllem5  25538  vitalilem1  25559  vitalilem5  25563  mbfconstlem  25578  mbfima  25581  mbfid  25586  ismbf2d  25591  mbfss  25597  mbfmulc2lem  25598  i1fd  25632  itg1addlem2  25648  itg1addlem4  25650  itg1addlem5  25651  i1fmulc  25654  itg2l  25680  itg2cl  25683  ibl0  25738  iblrelem  25742  iblpos  25744  iblss2  25757  bddmulibl  25790  bddiblnc  25793  recnperf  25856  ply1remlem  26120  fta1glem1  26123  fta1g  26125  elply  26150  plypf1  26167  coefv0  26203  coemulc  26210  fta1  26266  elqaalem2  26278  aannenlem2  26287  aalioulem3  26292  taylfvallem1  26314  tayl0  26319  ulm0  26350  logtayl  26619  atanrecl  26871  atanbnd  26886  harmonicbnd3  26968  ftalem7  27039  basellem5  27045  ppifi  27066  sqff1o  27142  1sgmprm  27160  logexprlim  27186  dchrelbasd  27200  dchr1re  27224  lgslem4  27261  lgsne0  27296  2sqlem9  27388  2sqlem10  27389  rpvmasumlem  27448  dchrisumlem1  27450  vmalogdivsum  27500  pntrlog2bndlem5  27542  ostth  27600  lrrecse  27892  ssltmul1  28090  ssltmul2  28091  mulsuniflem  28092  noseqex  28212  n0mulscl  28265  eln0s  28275  n0subs  28277  n0zs  28292  expscl  28330  elzs12  28338  tgcgr4  28456  axlowdimlem16  28882  fusgrfisbase  29253  vtxdg0e  29400  rgrusgrprc  29515  wwlksnfi  29834  trlsegvdeglem7  30153  eulerpathpr  30167  0blo  30719  nmlno0lem  30720  omlsilem  31329  pjoc1i  31358  nonbooli  31578  nmlnop0iALT  31922  unopbd  31942  leoprf2  32054  opsqrlem4  32070  opsqrlem5  32071  pjbdlni  32076  pjcmul1i  32128  mptiffisupp  32616  sgncl  32756  drngidlhash  33395  evl1deg1  33535  ply1dg1rt  33538  ply1dg3rt0irred  33541  m1pmeq  33542  lvecendof1f1o  33619  fldext2rspun  33669  constrabscl  33758  zarcmplem  33858  prsssdm  33894  ordtrestNEW  33898  esumpad  34032  esumpad2  34033  esumcst  34040  esumrnmpt2  34045  sibf0  34312  sitgclcn  34322  sitgclre  34323  eulerpartlemgs2  34358  dstfrvclim1  34456  ballotlemfelz  34469  signstfveq0  34555  breprexp  34611  wevgblacfn  35077  subfacp1lem3  35150  rellysconn  35219  cvmlift2lem9  35279  nnuni  35690  ordcmp  36411  bj-snex  36999  finxpreclem4  37358  poimirlem16  37606  poimirlem17  37607  voliunnfl  37634  mbfresfi  37636  itg2addnclem2  37642  dvasin  37674  heiborlem4  37784  heiborlem6  37786  itrere  42314  sn-itrere  42458  sn-retire  42459  wepwsolem  43013  flcidc  43141  iocmbl  43184  arearect  43186  omcl3g  43305  iscard4  43504  briunov2uz  43669  eliunov2uz  43670  frege124d  43732  frege129d  43734  frege92  43926  lhe4.4ex1a  44301  dvconstbi  44306  binomcxplemnn0  44321  binomcxplemnotnn0  44328  infxr  45342  infleinflem2  45346  climneg  45587  cncfiooicc  45871  itgsinexplem1  45931  volioof  45964  stoweidlem36  46013  wallispilem3  46044  fourierdlem93  46176  fouriersw  46208  fouriercn  46209  etransclem16  46227  etransclem33  46244  sge0reuz  46424  nnfoctbdjlem  46432  hoidmvlelem3  46574  upwordnul  46857  dfatafv2ex  47190  sprsymrelfvlem  47452  fmtnofz04prm  47539  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  gpg3nbgrvtx0  48026  lincext2  48379  blennn0elnn  48505  itcovalsucov  48596  resccat  48989  funcf2lem2  48995  isnatd  49091  swapfelvv  49128  fucoelvv  49179  prcofelvv  49238  prstcprs  49385