Theorem eqeltrdi 2839

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

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

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 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  eqeltrrdi  2840  csbexg  5246  unisn2  5248  class2set  5291  snexALT  5319  snex  5372  prex  5373  iotaex  6457  fvrn0  6850  f0cli  7031  funsneqopb  7085  fmptsng  7102  fmptsnd  7103  elimdelov  7442  ovima0  7525  ndmovcl  7531  caovmo  7583  soex  7851  zfrep6  7887  1st2ndb  7961  fprresex  8240  smofvon2  8276  tz7.44-2  8326  oesuclem  8440  omcl  8451  oecl  8452  nnmcl  8527  nnecl  8528  fsetex  8780  fsetexb  8788  ixpexg  8846  resixpfo  8860  xpsnen  8974  ssfi  9082  cnvfi  9085  nnunifi  9175  imafiOLD  9200  prfi  9208  fsuppun  9271  0fsupp  9274  oiexg  9421  hartogslem1  9428  cantnfvalf  9555  rnttrcl  9612  ttrclse  9617  rankdmr1  9694  rankr1c  9714  numwdom  9950  alephon  9960  isfin5  10190  sdom2en01  10193  isf32lem9  10252  hsmexlem9  10316  iundom2g  10431  gchxpidm  10560  r1tskina  10673  tskmcl  10732  recmulnq  10855  recclnq  10857  genpelv  10891  un0mulcl  12415  znegcl  12507  zeo  12559  eqreznegel  12832  xnegcl  13112  xnn0xaddcl  13134  ioorebas  13351  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  14705  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  18590  submnd0  18671  qusgrp2  18971  mulgfval  18982  issubg2  19054  triv1nsgd  19085  0subgALT  19480  torsubg  19766  frgpnabllem1  19785  lt6abl  19807  ablfaclem3  20001  ablfac2  20003  simpgnsgd  20014  qusrng  20098  srgbinomlem3  20146  ringidss  20195  qusring2  20252  isdrngd  20680  isdrngdOLD  20682  mptscmfsupp0  20860  islss3  20892  ellspsn  20936  lspprel  21028  znf1o  21488  frgpcyg  21510  cnmsgnsubg  21514  phlpropd  21592  cssval  21619  iscss  21620  dsmm0cl  21677  uvcvvcl  21724  m1detdiag  22512  m2detleiblem1  22539  pmatcollpw3fi1lem1  22701  indistopon  22916  indiscld  23006  restbas  23073  ordttopon  23108  iocpnfordt  23130  icomnfordt  23131  lecldbas  23134  fiuncmp  23319  cmpfi  23323  conncompid  23346  dissnlocfin  23444  elpt  23487  xkotop  23503  xkouni  23514  xkohaus  23568  xkoptsub  23569  imastopn  23635  filconn  23798  cfinufil  23843  alexsublem  23959  alexsub  23960  alexsubALTlem4  23965  distgp  24014  indistgp  24015  ssblps  24337  ssbl  24338  xmeter  24348  nmoi  24643  nmoeq0  24651  0nghm  24656  idnghm  24658  icccld  24681  iocmnfcld  24683  blssioo  24710  xrtgioo  24722  xrsxmet  24725  icccmp  24741  pcopt  24949  pcopt2  24950  elpi1  24972  cmetcaulem  25215  ishl2  25297  rrxmvallem  25331  ovolcl  25406  ovolunlem1a  25424  ovolunnul  25428  ovoliunnul  25435  ioombl1  25490  icombl  25492  ioombl  25493  iccmbl  25494  iccvolcl  25495  ovolioo  25496  ioovolcl  25498  ioorcl  25505  uniioovol  25507  uniioombllem2a  25510  uniioombllem4  25514  uniioombllem5  25515  vitalilem1  25536  vitalilem5  25540  mbfconstlem  25555  mbfima  25558  mbfid  25563  ismbf2d  25568  mbfss  25574  mbfmulc2lem  25575  i1fd  25609  itg1addlem2  25625  itg1addlem4  25627  itg1addlem5  25628  i1fmulc  25631  itg2l  25657  itg2cl  25660  ibl0  25715  iblrelem  25719  iblpos  25721  iblss2  25734  bddmulibl  25767  bddiblnc  25770  recnperf  25833  ply1remlem  26097  fta1glem1  26100  fta1g  26102  elply  26127  plypf1  26144  coefv0  26180  coemulc  26187  fta1  26243  elqaalem2  26255  aannenlem2  26264  aalioulem3  26269  taylfvallem1  26291  tayl0  26296  ulm0  26327  logtayl  26596  atanrecl  26848  atanbnd  26863  harmonicbnd3  26945  ftalem7  27016  basellem5  27022  ppifi  27043  sqff1o  27119  1sgmprm  27137  logexprlim  27163  dchrelbasd  27177  dchr1re  27201  lgslem4  27238  lgsne0  27273  2sqlem9  27365  2sqlem10  27366  rpvmasumlem  27425  dchrisumlem1  27427  vmalogdivsum  27477  pntrlog2bndlem5  27519  ostth  27577  lrrecse  27885  ssltmul1  28086  ssltmul2  28087  mulsuniflem  28088  noseqex  28219  n0mulscl  28273  n0sfincut  28282  eln0s  28287  n0subs  28289  n0zs  28313  expscllem  28353  elzs12  28383  tgcgr4  28509  axlowdimlem16  28935  fusgrfisbase  29306  vtxdg0e  29453  rgrusgrprc  29568  wwlksnfi  29884  trlsegvdeglem7  30206  eulerpathpr  30220  0blo  30772  nmlno0lem  30773  omlsilem  31382  pjoc1i  31411  nonbooli  31631  nmlnop0iALT  31975  unopbd  31995  leoprf2  32107  opsqrlem4  32123  opsqrlem5  32124  pjbdlni  32129  pjcmul1i  32181  mptiffisupp  32674  sgncl  32814  drngidlhash  33399  evl1deg1  33539  ply1dg1rt  33543  ply1dg3rt0irred  33546  m1pmeq  33547  lvecendof1f1o  33646  fldext2rspun  33695  constrabscl  33791  zarcmplem  33894  prsssdm  33930  ordtrestNEW  33934  esumpad  34068  esumpad2  34069  esumcst  34076  esumrnmpt2  34081  sibf0  34347  sitgclcn  34357  sitgclre  34358  eulerpartlemgs2  34393  dstfrvclim1  34491  ballotlemfelz  34504  signstfveq0  34590  breprexp  34646  r1wf  35107  fineqvnttrclselem1  35141  wevgblacfn  35153  subfacp1lem3  35226  rellysconn  35295  cvmlift2lem9  35355  nnuni  35771  ordcmp  36489  bj-snex  37077  finxpreclem4  37436  poimirlem16  37684  poimirlem17  37685  voliunnfl  37712  mbfresfi  37714  itg2addnclem2  37720  dvasin  37752  heiborlem4  37862  heiborlem6  37864  itrere  42359  sn-itrere  42529  sn-retire  42530  wepwsolem  43083  flcidc  43211  iocmbl  43254  arearect  43256  omcl3g  43375  iscard4  43574  briunov2uz  43739  eliunov2uz  43740  frege124d  43802  frege129d  43804  frege92  43996  lhe4.4ex1a  44370  dvconstbi  44375  binomcxplemnn0  44390  binomcxplemnotnn0  44397  infxr  45413  infleinflem2  45417  climneg  45658  cncfiooicc  45940  itgsinexplem1  46000  volioof  46033  stoweidlem36  46082  wallispilem3  46113  fourierdlem93  46245  fouriersw  46277  fouriercn  46278  etransclem16  46296  etransclem33  46313  sge0reuz  46493  nnfoctbdjlem  46501  hoidmvlelem3  46643  sinnpoly  46930  dfatafv2ex  47252  sprsymrelfvlem  47529  fmtnofz04prm  47616  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  gpg3nbgrvtx0  48115  lincext2  48495  blennn0elnn  48617  itcovalsucov  48708  resccat  49114  funcf2lem2  49122  isnatd  49263  swapfelvv  49303  fucoelvv  49360  prcofelvv  49420  termco  49521  prstcprs  49600