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  5249  unisn2  5251  class2set  5294  snexALT  5322  snex  5375  prex  5376  iotaex  6458  fvrn0  6850  f0cli  7032  funsneqopb  7086  fmptsng  7104  fmptsnd  7105  elimdelov  7445  ovima0  7528  ndmovcl  7534  caovmo  7586  soex  7854  zfrep6  7890  1st2ndb  7964  fprresex  8243  smofvon2  8279  tz7.44-2  8329  oesuclem  8443  omcl  8454  oecl  8455  nnmcl  8530  nnecl  8531  fsetex  8783  fsetexb  8791  ixpexg  8849  resixpfo  8863  xpsnen  8978  ssfi  9087  cnvfi  9090  nnunifi  9180  imafiOLD  9205  prfi  9213  fsuppun  9277  0fsupp  9280  oiexg  9427  hartogslem1  9434  cantnfvalf  9561  rnttrcl  9618  ttrclse  9623  rankdmr1  9697  rankr1c  9717  numwdom  9953  alephon  9963  isfin5  10193  sdom2en01  10196  isf32lem9  10255  hsmexlem9  10319  iundom2g  10434  gchxpidm  10563  r1tskina  10676  tskmcl  10735  recmulnq  10858  recclnq  10860  genpelv  10894  un0mulcl  12418  znegcl  12510  zeo  12562  eqreznegel  12835  xnegcl  13115  xnn0xaddcl  13137  ioorebas  13354  modid0  13801  2txmodxeq0  13838  fzofi  13881  seqexw  13924  expcllem  13979  m1expcl2  13992  faclbnd4lem3  14202  bccl  14229  hasheq0  14270  hashrabrsn  14279  fnfz0hashnn0  14355  fnfzo0hashnn0  14358  wrdnfi  14455  cshwcl  14704  relexpaddg  14960  abs00bd  15198  iserge0  15568  sumrblem  15618  fsumcvg  15619  summolem2a  15622  sumss  15631  fsumss  15632  fsumcvg2  15634  sumsplit  15675  binom  15737  bcxmas  15742  geomulcvg  15783  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  zprod  15844  fprodntriv  15849  prodss  15854  fprodss  15855  binomfallfac  15948  bpoly1  15958  bpoly2  15964  bpoly3  15965  ruclem6  16144  smupf  16389  gcdcl  16417  lcmcl  16512  lcmfcl  16539  2mulprm  16604  pcxnn0cl  16772  pcxcl  16773  pcmptcl  16803  infpnlem2  16823  zgz  16845  4sqlem2  16861  4sqlem19  16875  vdwapval  16885  hashbc0  16917  ramcl2  16928  0ramcl  16935  ramcl  16941  isstruct2  17060  imasval  17415  imasbas  17416  imasds  17417  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  imasle  17427  qusaddvallem  17455  qusaddflem  17456  qusaddval  17457  qusaddf  17458  qusmulval  17459  qusmulf  17460  mreexexlem3d  17552  sscpwex  17722  fullresc  17758  estrres  18045  evlfcl  18128  ipopos  18442  gsumress  18556  submnd0  18637  qusgrp2  18937  mulgfval  18948  issubg2  19020  triv1nsgd  19052  0subgALT  19447  torsubg  19733  frgpnabllem1  19752  lt6abl  19774  ablfaclem3  19968  ablfac2  19970  simpgnsgd  19981  qusrng  20065  srgbinomlem3  20113  ringidss  20162  qusring2  20219  isdrngd  20650  isdrngdOLD  20652  mptscmfsupp0  20830  islss3  20862  ellspsn  20906  lspprel  20998  znf1o  21458  frgpcyg  21480  cnmsgnsubg  21484  phlpropd  21562  cssval  21589  iscss  21590  dsmm0cl  21647  uvcvvcl  21694  m1detdiag  22482  m2detleiblem1  22509  pmatcollpw3fi1lem1  22671  indistopon  22886  indiscld  22976  restbas  23043  ordttopon  23078  iocpnfordt  23100  icomnfordt  23101  lecldbas  23104  fiuncmp  23289  cmpfi  23293  conncompid  23316  dissnlocfin  23414  elpt  23457  xkotop  23473  xkouni  23484  xkohaus  23538  xkoptsub  23539  imastopn  23605  filconn  23768  cfinufil  23813  alexsublem  23929  alexsub  23930  alexsubALTlem4  23935  distgp  23984  indistgp  23985  ssblps  24308  ssbl  24309  xmeter  24319  nmoi  24614  nmoeq0  24622  0nghm  24627  idnghm  24629  icccld  24652  iocmnfcld  24654  blssioo  24681  xrtgioo  24693  xrsxmet  24696  icccmp  24712  pcopt  24920  pcopt2  24921  elpi1  24943  cmetcaulem  25186  ishl2  25268  rrxmvallem  25302  ovolcl  25377  ovolunlem1a  25395  ovolunnul  25399  ovoliunnul  25406  ioombl1  25461  icombl  25463  ioombl  25464  iccmbl  25465  iccvolcl  25466  ovolioo  25467  ioovolcl  25469  ioorcl  25476  uniioovol  25478  uniioombllem2a  25481  uniioombllem4  25485  uniioombllem5  25486  vitalilem1  25507  vitalilem5  25511  mbfconstlem  25526  mbfima  25529  mbfid  25534  ismbf2d  25539  mbfss  25545  mbfmulc2lem  25546  i1fd  25580  itg1addlem2  25596  itg1addlem4  25598  itg1addlem5  25599  i1fmulc  25602  itg2l  25628  itg2cl  25631  ibl0  25686  iblrelem  25690  iblpos  25692  iblss2  25705  bddmulibl  25738  bddiblnc  25741  recnperf  25804  ply1remlem  26068  fta1glem1  26071  fta1g  26073  elply  26098  plypf1  26115  coefv0  26151  coemulc  26158  fta1  26214  elqaalem2  26226  aannenlem2  26235  aalioulem3  26240  taylfvallem1  26262  tayl0  26267  ulm0  26298  logtayl  26567  atanrecl  26819  atanbnd  26834  harmonicbnd3  26916  ftalem7  26987  basellem5  26993  ppifi  27014  sqff1o  27090  1sgmprm  27108  logexprlim  27134  dchrelbasd  27148  dchr1re  27172  lgslem4  27209  lgsne0  27244  2sqlem9  27336  2sqlem10  27337  rpvmasumlem  27396  dchrisumlem1  27398  vmalogdivsum  27448  pntrlog2bndlem5  27490  ostth  27548  lrrecse  27854  ssltmul1  28055  ssltmul2  28056  mulsuniflem  28057  noseqex  28188  n0mulscl  28242  n0sfincut  28251  eln0s  28256  n0subs  28258  n0zs  28282  expscllem  28322  elzs12  28350  tgcgr4  28476  axlowdimlem16  28902  fusgrfisbase  29273  vtxdg0e  29420  rgrusgrprc  29535  wwlksnfi  29851  trlsegvdeglem7  30170  eulerpathpr  30184  0blo  30736  nmlno0lem  30737  omlsilem  31346  pjoc1i  31375  nonbooli  31595  nmlnop0iALT  31939  unopbd  31959  leoprf2  32071  opsqrlem4  32087  opsqrlem5  32088  pjbdlni  32093  pjcmul1i  32145  mptiffisupp  32635  sgncl  32776  drngidlhash  33371  evl1deg1  33511  ply1dg1rt  33515  ply1dg3rt0irred  33518  m1pmeq  33519  lvecendof1f1o  33600  fldext2rspun  33649  constrabscl  33745  zarcmplem  33848  prsssdm  33884  ordtrestNEW  33888  esumpad  34022  esumpad2  34023  esumcst  34030  esumrnmpt2  34035  sibf0  34302  sitgclcn  34312  sitgclre  34313  eulerpartlemgs2  34348  dstfrvclim1  34446  ballotlemfelz  34459  signstfveq0  34545  breprexp  34601  wevgblacfn  35082  subfacp1lem3  35155  rellysconn  35224  cvmlift2lem9  35284  nnuni  35700  ordcmp  36421  bj-snex  37009  finxpreclem4  37368  poimirlem16  37616  poimirlem17  37617  voliunnfl  37644  mbfresfi  37646  itg2addnclem2  37652  dvasin  37684  heiborlem4  37794  heiborlem6  37796  itrere  42291  sn-itrere  42461  sn-retire  42462  wepwsolem  43015  flcidc  43143  iocmbl  43186  arearect  43188  omcl3g  43307  iscard4  43506  briunov2uz  43671  eliunov2uz  43672  frege124d  43734  frege129d  43736  frege92  43928  lhe4.4ex1a  44302  dvconstbi  44307  binomcxplemnn0  44322  binomcxplemnotnn0  44329  infxr  45346  infleinflem2  45350  climneg  45591  cncfiooicc  45875  itgsinexplem1  45935  volioof  45968  stoweidlem36  46017  wallispilem3  46048  fourierdlem93  46180  fouriersw  46212  fouriercn  46213  etransclem16  46231  etransclem33  46248  sge0reuz  46428  nnfoctbdjlem  46436  hoidmvlelem3  46578  upwordnul  46861  sinnpoly  46875  dfatafv2ex  47197  sprsymrelfvlem  47474  fmtnofz04prm  47561  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  gpg3nbgrvtx0  48060  lincext2  48440  blennn0elnn  48562  itcovalsucov  48653  resccat  49059  funcf2lem2  49067  isnatd  49208  swapfelvv  49248  fucoelvv  49305  prcofelvv  49365  termco  49466  prstcprs  49545