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 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eqeltrrdi  2843  csbexg  5310  unisn2  5312  class2set  5353  snexALT  5381  snex  5431  prex  5432  iotaex  6514  iotaexOLD  6521  fvrn0  6919  f0cli  7097  funsneqopb  7147  fmptsng  7163  fmptsnd  7164  elimdelov  7502  ovima0  7583  ndmovcl  7589  caovmo  7641  soex  7909  zfrep6  7938  1st2ndb  8012  fprresex  8292  wfrlem17OLD  8322  smofvon2  8353  tz7.44-2  8404  oesuclem  8522  omcl  8533  oecl  8534  nnmcl  8609  nnecl  8610  fsetex  8847  fsetexb  8855  ixpexg  8913  resixpfo  8927  en1bOLD  9021  xpsnen  9052  ssfi  9170  imafi  9172  cnvfi  9177  nnunifi  9291  xpfiOLD  9315  fsuppun  9379  0fsupp  9382  oiexg  9527  hartogslem1  9534  cantnfvalf  9657  rnttrcl  9714  ttrclse  9719  rankdmr1  9793  rankr1c  9813  numwdom  10051  alephon  10061  isfin5  10291  sdom2en01  10294  isf32lem9  10353  hsmexlem9  10417  iundom2g  10532  gchxpidm  10661  r1tskina  10774  tskmcl  10833  recmulnq  10956  recclnq  10958  genpelv  10992  un0mulcl  12503  znegcl  12594  zeo  12645  eqreznegel  12915  xnegcl  13189  xnn0xaddcl  13211  ioorebas  13425  modid0  13859  2txmodxeq0  13893  fzofi  13936  seqexw  13979  expcllem  14035  m1expcl2  14048  faclbnd4lem3  14252  bccl  14279  hasheq0  14320  hashrabrsn  14329  fnfz0hashnn0  14404  fnfzo0hashnn0  14407  wrdnfi  14495  cshwcl  14745  relexpaddg  14997  abs00bd  15235  iserge0  15604  sumrblem  15654  fsumcvg  15655  summolem2a  15658  sumss  15667  fsumss  15668  fsumcvg2  15670  sumsplit  15711  binom  15773  bcxmas  15778  geomulcvg  15819  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  zprod  15878  fprodntriv  15883  prodss  15888  fprodss  15889  binomfallfac  15982  bpoly1  15992  bpoly2  15998  bpoly3  15999  ruclem6  16175  smupf  16416  gcdcl  16444  lcmcl  16535  lcmfcl  16562  2mulprm  16627  pcxnn0cl  16790  pcxcl  16791  pcmptcl  16821  infpnlem2  16841  zgz  16863  4sqlem2  16879  4sqlem19  16893  vdwapval  16903  hashbc0  16935  ramcl2  16946  0ramcl  16953  ramcl  16959  isstruct2  17079  imasval  17454  imasbas  17455  imasds  17456  imasplusg  17460  imasmulr  17461  imasvsca  17463  imasip  17464  imasle  17466  qusaddvallem  17494  qusaddflem  17495  qusaddval  17496  qusaddf  17497  qusmulval  17498  qusmulf  17499  mreexexlem3d  17587  sscpwex  17759  fullresc  17798  estrres  18088  evlfcl  18172  ipopos  18486  gsumress  18598  submnd0  18651  qusgrp2  18938  mulgfval  18947  issubg2  19016  triv1nsgd  19048  0subgALT  19431  torsubg  19717  frgpnabllem1  19736  lt6abl  19758  ablfaclem3  19952  ablfac2  19954  simpgnsgd  19965  srgbinomlem3  20045  ringidss  20088  qusring2  20140  isdrngd  20341  isdrngdOLD  20343  mptscmfsupp0  20530  islss3  20563  lspsnel  20607  lspprel  20698  znf1o  21099  frgpcyg  21121  cnmsgnsubg  21122  phlpropd  21200  cssval  21227  iscss  21228  dsmm0cl  21287  uvcvvcl  21334  m1detdiag  22091  m2detleiblem1  22118  pmatcollpw3fi1lem1  22280  indistopon  22496  indiscld  22587  restbas  22654  ordttopon  22689  iocpnfordt  22711  icomnfordt  22712  lecldbas  22715  fiuncmp  22900  cmpfi  22904  conncompid  22927  dissnlocfin  23025  elpt  23068  xkotop  23084  xkouni  23095  xkohaus  23149  xkoptsub  23150  imastopn  23216  filconn  23379  cfinufil  23424  alexsublem  23540  alexsub  23541  alexsubALTlem4  23546  distgp  23595  indistgp  23596  ssblps  23920  ssbl  23921  xmeter  23931  nmoi  24237  nmoeq0  24245  0nghm  24250  idnghm  24252  icccld  24275  iocmnfcld  24277  blssioo  24303  xrtgioo  24314  xrsxmet  24317  icccmp  24333  pcopt  24530  pcopt2  24531  elpi1  24553  cmetcaulem  24797  ishl2  24879  rrxmvallem  24913  ovolcl  24987  ovolunlem1a  25005  ovolunnul  25009  ovoliunnul  25016  ioombl1  25071  icombl  25073  ioombl  25074  iccmbl  25075  iccvolcl  25076  ovolioo  25077  ioovolcl  25079  ioorcl  25086  uniioovol  25088  uniioombllem2a  25091  uniioombllem4  25095  uniioombllem5  25096  vitalilem1  25117  vitalilem5  25121  mbfconstlem  25136  mbfima  25139  mbfid  25144  ismbf2d  25149  mbfss  25155  mbfmulc2lem  25156  i1fd  25190  itg1addlem2  25206  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  i1fmulc  25213  itg2l  25239  itg2cl  25242  ibl0  25296  iblrelem  25300  iblpos  25302  iblss2  25315  bddmulibl  25348  bddiblnc  25351  recnperf  25414  ply1remlem  25672  fta1glem1  25675  fta1g  25677  elply  25701  plypf1  25718  coefv0  25754  coemulc  25761  fta1  25813  elqaalem2  25825  aannenlem2  25834  aalioulem3  25839  taylfvallem1  25861  tayl0  25866  ulm0  25895  logtayl  26160  atanrecl  26406  atanbnd  26421  harmonicbnd3  26502  ftalem7  26573  basellem5  26579  ppifi  26600  sqff1o  26676  1sgmprm  26692  logexprlim  26718  dchrelbasd  26732  dchr1re  26756  lgslem4  26793  lgsne0  26828  2sqlem9  26920  2sqlem10  26921  rpvmasumlem  26980  dchrisumlem1  26982  vmalogdivsum  27032  pntrlog2bndlem5  27074  ostth  27132  lrrecse  27416  ssltmul1  27592  ssltmul2  27593  mulsuniflem  27594  tgcgr4  27772  axlowdimlem16  28205  fusgrfisbase  28575  vtxdg0e  28721  rgrusgrprc  28836  wwlksnfi  29150  trlsegvdeglem7  29469  eulerpathpr  29483  0blo  30033  nmlno0lem  30034  omlsilem  30643  pjoc1i  30672  nonbooli  30892  nmlnop0iALT  31236  unopbd  31256  leoprf2  31368  opsqrlem4  31384  opsqrlem5  31385  pjbdlni  31390  pjcmul1i  31442  mptiffisupp  31903  drngidlhash  32541  zarcmplem  32850  prsssdm  32886  ordtrestNEW  32890  esumpad  33042  esumpad2  33043  esumcst  33050  esumrnmpt2  33055  sibf0  33322  sitgclcn  33332  sitgclre  33333  eulerpartlemgs2  33368  dstfrvclim1  33465  ballotlemfelz  33478  sgncl  33526  signstfveq0  33577  breprexp  33634  subfacp1lem3  34162  rellysconn  34231  cvmlift2lem9  34291  nnuni  34685  ordcmp  35321  bj-snex  35905  finxpreclem4  36264  poimirlem16  36493  poimirlem17  36494  voliunnfl  36521  mbfresfi  36523  itg2addnclem2  36529  dvasin  36561  heiborlem4  36671  heiborlem6  36673  itrere  41336  retire  41337  wepwsolem  41770  flcidc  41902  iocmbl  41948  arearect  41950  omcl3g  42070  iscard4  42270  briunov2uz  42435  eliunov2uz  42436  frege124d  42498  frege129d  42500  frege92  42692  lhe4.4ex1a  43074  dvconstbi  43079  binomcxplemnn0  43094  binomcxplemnotnn0  43101  infxr  44064  infleinflem2  44068  climneg  44313  cncfiooicc  44597  itgsinexplem1  44657  volioof  44690  stoweidlem36  44739  wallispilem3  44770  fourierdlem93  44902  fouriersw  44934  fouriercn  44935  etransclem16  44953  etransclem33  44970  sge0reuz  45150  nnfoctbdjlem  45158  hoidmvlelem3  45300  upwordnul  45581  dfatafv2ex  45908  sprsymrelfvlem  46145  fmtnofz04prm  46232  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  qusrng  46668  lincext2  47090  blennn0elnn  47217  itcovalsucov  47308  prstcprs  47649