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  5311  unisn2  5313  class2set  5354  snexALT  5382  snex  5432  prex  5433  iotaex  6517  iotaexOLD  6524  fvrn0  6922  f0cli  7100  funsneqopb  7150  fmptsng  7166  fmptsnd  7167  elimdelov  7505  ovima0  7586  ndmovcl  7592  caovmo  7644  soex  7912  zfrep6  7941  1st2ndb  8015  fprresex  8295  wfrlem17OLD  8325  smofvon2  8356  tz7.44-2  8407  oesuclem  8525  omcl  8536  oecl  8537  nnmcl  8612  nnecl  8613  fsetex  8850  fsetexb  8858  ixpexg  8916  resixpfo  8930  en1bOLD  9024  xpsnen  9055  ssfi  9173  imafi  9175  cnvfi  9180  nnunifi  9294  xpfiOLD  9318  fsuppun  9382  0fsupp  9385  oiexg  9530  hartogslem1  9537  cantnfvalf  9660  rnttrcl  9717  ttrclse  9722  rankdmr1  9796  rankr1c  9816  numwdom  10054  alephon  10064  isfin5  10294  sdom2en01  10297  isf32lem9  10356  hsmexlem9  10420  iundom2g  10535  gchxpidm  10664  r1tskina  10777  tskmcl  10836  recmulnq  10959  recclnq  10961  genpelv  10995  un0mulcl  12506  znegcl  12597  zeo  12648  eqreznegel  12918  xnegcl  13192  xnn0xaddcl  13214  ioorebas  13428  modid0  13862  2txmodxeq0  13896  fzofi  13939  seqexw  13982  expcllem  14038  m1expcl2  14051  faclbnd4lem3  14255  bccl  14282  hasheq0  14323  hashrabrsn  14332  fnfz0hashnn0  14407  fnfzo0hashnn0  14410  wrdnfi  14498  cshwcl  14748  relexpaddg  15000  abs00bd  15238  iserge0  15607  sumrblem  15657  fsumcvg  15658  summolem2a  15661  sumss  15670  fsumss  15671  fsumcvg2  15673  sumsplit  15714  binom  15776  bcxmas  15781  geomulcvg  15822  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  fprodntriv  15886  prodss  15891  fprodss  15892  binomfallfac  15985  bpoly1  15995  bpoly2  16001  bpoly3  16002  ruclem6  16178  smupf  16419  gcdcl  16447  lcmcl  16538  lcmfcl  16565  2mulprm  16630  pcxnn0cl  16793  pcxcl  16794  pcmptcl  16824  infpnlem2  16844  zgz  16866  4sqlem2  16882  4sqlem19  16896  vdwapval  16906  hashbc0  16938  ramcl2  16949  0ramcl  16956  ramcl  16962  isstruct2  17082  imasval  17457  imasbas  17458  imasds  17459  imasplusg  17463  imasmulr  17464  imasvsca  17466  imasip  17467  imasle  17469  qusaddvallem  17497  qusaddflem  17498  qusaddval  17499  qusaddf  17500  qusmulval  17501  qusmulf  17502  mreexexlem3d  17590  sscpwex  17762  fullresc  17801  estrres  18091  evlfcl  18175  ipopos  18489  gsumress  18601  submnd0  18654  qusgrp2  18941  mulgfval  18952  issubg2  19021  triv1nsgd  19053  0subgALT  19436  torsubg  19722  frgpnabllem1  19741  lt6abl  19763  ablfaclem3  19957  ablfac2  19959  simpgnsgd  19970  srgbinomlem3  20051  ringidss  20094  qusring2  20147  isdrngd  20390  isdrngdOLD  20392  mptscmfsupp0  20537  islss3  20570  lspsnel  20614  lspprel  20705  znf1o  21107  frgpcyg  21129  cnmsgnsubg  21130  phlpropd  21208  cssval  21235  iscss  21236  dsmm0cl  21295  uvcvvcl  21342  m1detdiag  22099  m2detleiblem1  22126  pmatcollpw3fi1lem1  22288  indistopon  22504  indiscld  22595  restbas  22662  ordttopon  22697  iocpnfordt  22719  icomnfordt  22720  lecldbas  22723  fiuncmp  22908  cmpfi  22912  conncompid  22935  dissnlocfin  23033  elpt  23076  xkotop  23092  xkouni  23103  xkohaus  23157  xkoptsub  23158  imastopn  23224  filconn  23387  cfinufil  23432  alexsublem  23548  alexsub  23549  alexsubALTlem4  23554  distgp  23603  indistgp  23604  ssblps  23928  ssbl  23929  xmeter  23939  nmoi  24245  nmoeq0  24253  0nghm  24258  idnghm  24260  icccld  24283  iocmnfcld  24285  blssioo  24311  xrtgioo  24322  xrsxmet  24325  icccmp  24341  pcopt  24538  pcopt2  24539  elpi1  24561  cmetcaulem  24805  ishl2  24887  rrxmvallem  24921  ovolcl  24995  ovolunlem1a  25013  ovolunnul  25017  ovoliunnul  25024  ioombl1  25079  icombl  25081  ioombl  25082  iccmbl  25083  iccvolcl  25084  ovolioo  25085  ioovolcl  25087  ioorcl  25094  uniioovol  25096  uniioombllem2a  25099  uniioombllem4  25103  uniioombllem5  25104  vitalilem1  25125  vitalilem5  25129  mbfconstlem  25144  mbfima  25147  mbfid  25152  ismbf2d  25157  mbfss  25163  mbfmulc2lem  25164  i1fd  25198  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  i1fmulc  25221  itg2l  25247  itg2cl  25250  ibl0  25304  iblrelem  25308  iblpos  25310  iblss2  25323  bddmulibl  25356  bddiblnc  25359  recnperf  25422  ply1remlem  25680  fta1glem1  25683  fta1g  25685  elply  25709  plypf1  25726  coefv0  25762  coemulc  25769  fta1  25821  elqaalem2  25833  aannenlem2  25842  aalioulem3  25847  taylfvallem1  25869  tayl0  25874  ulm0  25903  logtayl  26168  atanrecl  26416  atanbnd  26431  harmonicbnd3  26512  ftalem7  26583  basellem5  26589  ppifi  26610  sqff1o  26686  1sgmprm  26702  logexprlim  26728  dchrelbasd  26742  dchr1re  26766  lgslem4  26803  lgsne0  26838  2sqlem9  26930  2sqlem10  26931  rpvmasumlem  26990  dchrisumlem1  26992  vmalogdivsum  27042  pntrlog2bndlem5  27084  ostth  27142  lrrecse  27426  ssltmul1  27602  ssltmul2  27603  mulsuniflem  27604  tgcgr4  27782  axlowdimlem16  28215  fusgrfisbase  28585  vtxdg0e  28731  rgrusgrprc  28846  wwlksnfi  29160  trlsegvdeglem7  29479  eulerpathpr  29493  0blo  30045  nmlno0lem  30046  omlsilem  30655  pjoc1i  30684  nonbooli  30904  nmlnop0iALT  31248  unopbd  31268  leoprf2  31380  opsqrlem4  31396  opsqrlem5  31397  pjbdlni  31402  pjcmul1i  31454  mptiffisupp  31915  drngidlhash  32552  zarcmplem  32861  prsssdm  32897  ordtrestNEW  32901  esumpad  33053  esumpad2  33054  esumcst  33061  esumrnmpt2  33066  sibf0  33333  sitgclcn  33343  sitgclre  33344  eulerpartlemgs2  33379  dstfrvclim1  33476  ballotlemfelz  33489  sgncl  33537  signstfveq0  33588  breprexp  33645  subfacp1lem3  34173  rellysconn  34242  cvmlift2lem9  34302  nnuni  34696  ordcmp  35332  bj-snex  35916  finxpreclem4  36275  poimirlem16  36504  poimirlem17  36505  voliunnfl  36532  mbfresfi  36534  itg2addnclem2  36540  dvasin  36572  heiborlem4  36682  heiborlem6  36684  itrere  41339  retire  41340  wepwsolem  41784  flcidc  41916  iocmbl  41962  arearect  41964  omcl3g  42084  iscard4  42284  briunov2uz  42449  eliunov2uz  42450  frege124d  42512  frege129d  42514  frege92  42706  lhe4.4ex1a  43088  dvconstbi  43093  binomcxplemnn0  43108  binomcxplemnotnn0  43115  infxr  44077  infleinflem2  44081  climneg  44326  cncfiooicc  44610  itgsinexplem1  44670  volioof  44703  stoweidlem36  44752  wallispilem3  44783  fourierdlem93  44915  fouriersw  44947  fouriercn  44948  etransclem16  44966  etransclem33  44983  sge0reuz  45163  nnfoctbdjlem  45171  hoidmvlelem3  45313  upwordnul  45594  dfatafv2ex  45921  sprsymrelfvlem  46158  fmtnofz04prm  46245  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  qusrng  46681  lincext2  47136  blennn0elnn  47263  itcovalsucov  47354  prstcprs  47695