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  5260  unisn2  5262  class2set  5305  snexALT  5333  snex  5386  prex  5387  iotaex  6472  iotaexOLD  6479  fvrn0  6870  f0cli  7052  funsneqopb  7106  fmptsng  7124  fmptsnd  7125  elimdelov  7465  ovima0  7548  ndmovcl  7554  caovmo  7606  soex  7877  zfrep6  7913  1st2ndb  7987  fprresex  8266  smofvon2  8302  tz7.44-2  8352  oesuclem  8466  omcl  8477  oecl  8478  nnmcl  8553  nnecl  8554  fsetex  8806  fsetexb  8814  ixpexg  8872  resixpfo  8886  xpsnen  9002  ssfi  9114  cnvfi  9117  nnunifi  9214  imafiOLD  9241  xpfiOLD  9246  prfi  9250  fsuppun  9314  0fsupp  9317  oiexg  9464  hartogslem1  9471  cantnfvalf  9594  rnttrcl  9651  ttrclse  9656  rankdmr1  9730  rankr1c  9750  numwdom  9988  alephon  9998  isfin5  10228  sdom2en01  10231  isf32lem9  10290  hsmexlem9  10354  iundom2g  10469  gchxpidm  10598  r1tskina  10711  tskmcl  10770  recmulnq  10893  recclnq  10895  genpelv  10929  un0mulcl  12452  znegcl  12544  zeo  12596  eqreznegel  12869  xnegcl  13149  xnn0xaddcl  13171  ioorebas  13388  modid0  13835  2txmodxeq0  13872  fzofi  13915  seqexw  13958  expcllem  14013  m1expcl2  14026  faclbnd4lem3  14236  bccl  14263  hasheq0  14304  hashrabrsn  14313  fnfz0hashnn0  14389  fnfzo0hashnn0  14392  wrdnfi  14489  cshwcl  14739  relexpaddg  14995  abs00bd  15233  iserge0  15603  sumrblem  15653  fsumcvg  15654  summolem2a  15657  sumss  15666  fsumss  15667  fsumcvg2  15669  sumsplit  15710  binom  15772  bcxmas  15777  geomulcvg  15818  prodrblem  15871  fprodcvg  15872  prodmolem2a  15876  zprod  15879  fprodntriv  15884  prodss  15889  fprodss  15890  binomfallfac  15983  bpoly1  15993  bpoly2  15999  bpoly3  16000  ruclem6  16179  smupf  16424  gcdcl  16452  lcmcl  16547  lcmfcl  16574  2mulprm  16639  pcxnn0cl  16807  pcxcl  16808  pcmptcl  16838  infpnlem2  16858  zgz  16880  4sqlem2  16896  4sqlem19  16910  vdwapval  16920  hashbc0  16952  ramcl2  16963  0ramcl  16970  ramcl  16976  isstruct2  17095  imasval  17450  imasbas  17451  imasds  17452  imasplusg  17456  imasmulr  17457  imasvsca  17459  imasip  17460  imasle  17462  qusaddvallem  17490  qusaddflem  17491  qusaddval  17492  qusaddf  17493  qusmulval  17494  qusmulf  17495  mreexexlem3d  17583  sscpwex  17753  fullresc  17789  estrres  18076  evlfcl  18159  ipopos  18471  gsumress  18585  submnd0  18666  qusgrp2  18966  mulgfval  18977  issubg2  19049  triv1nsgd  19081  0subgALT  19474  torsubg  19760  frgpnabllem1  19779  lt6abl  19801  ablfaclem3  19995  ablfac2  19997  simpgnsgd  20008  qusrng  20065  srgbinomlem3  20113  ringidss  20162  qusring2  20219  isdrngd  20650  isdrngdOLD  20652  mptscmfsupp0  20809  islss3  20841  ellspsn  20885  lspprel  20977  znf1o  21437  frgpcyg  21459  cnmsgnsubg  21462  phlpropd  21540  cssval  21567  iscss  21568  dsmm0cl  21625  uvcvvcl  21672  m1detdiag  22460  m2detleiblem1  22487  pmatcollpw3fi1lem1  22649  indistopon  22864  indiscld  22954  restbas  23021  ordttopon  23056  iocpnfordt  23078  icomnfordt  23079  lecldbas  23082  fiuncmp  23267  cmpfi  23271  conncompid  23294  dissnlocfin  23392  elpt  23435  xkotop  23451  xkouni  23462  xkohaus  23516  xkoptsub  23517  imastopn  23583  filconn  23746  cfinufil  23791  alexsublem  23907  alexsub  23908  alexsubALTlem4  23913  distgp  23962  indistgp  23963  ssblps  24286  ssbl  24287  xmeter  24297  nmoi  24592  nmoeq0  24600  0nghm  24605  idnghm  24607  icccld  24630  iocmnfcld  24632  blssioo  24659  xrtgioo  24671  xrsxmet  24674  icccmp  24690  pcopt  24898  pcopt2  24899  elpi1  24921  cmetcaulem  25164  ishl2  25246  rrxmvallem  25280  ovolcl  25355  ovolunlem1a  25373  ovolunnul  25377  ovoliunnul  25384  ioombl1  25439  icombl  25441  ioombl  25442  iccmbl  25443  iccvolcl  25444  ovolioo  25445  ioovolcl  25447  ioorcl  25454  uniioovol  25456  uniioombllem2a  25459  uniioombllem4  25463  uniioombllem5  25464  vitalilem1  25485  vitalilem5  25489  mbfconstlem  25504  mbfima  25507  mbfid  25512  ismbf2d  25517  mbfss  25523  mbfmulc2lem  25524  i1fd  25558  itg1addlem2  25574  itg1addlem4  25576  itg1addlem5  25577  i1fmulc  25580  itg2l  25606  itg2cl  25609  ibl0  25664  iblrelem  25668  iblpos  25670  iblss2  25683  bddmulibl  25716  bddiblnc  25719  recnperf  25782  ply1remlem  26046  fta1glem1  26049  fta1g  26051  elply  26076  plypf1  26093  coefv0  26129  coemulc  26136  fta1  26192  elqaalem2  26204  aannenlem2  26213  aalioulem3  26218  taylfvallem1  26240  tayl0  26245  ulm0  26276  logtayl  26545  atanrecl  26797  atanbnd  26812  harmonicbnd3  26894  ftalem7  26965  basellem5  26971  ppifi  26992  sqff1o  27068  1sgmprm  27086  logexprlim  27112  dchrelbasd  27126  dchr1re  27150  lgslem4  27187  lgsne0  27222  2sqlem9  27314  2sqlem10  27315  rpvmasumlem  27374  dchrisumlem1  27376  vmalogdivsum  27426  pntrlog2bndlem5  27468  ostth  27526  lrrecse  27825  ssltmul1  28026  ssltmul2  28027  mulsuniflem  28028  noseqex  28159  n0mulscl  28213  n0sfincut  28222  eln0s  28227  n0subs  28229  n0zs  28253  expscllem  28292  elzs12  28313  tgcgr4  28434  axlowdimlem16  28860  fusgrfisbase  29231  vtxdg0e  29378  rgrusgrprc  29493  wwlksnfi  29809  trlsegvdeglem7  30128  eulerpathpr  30142  0blo  30694  nmlno0lem  30695  omlsilem  31304  pjoc1i  31333  nonbooli  31553  nmlnop0iALT  31897  unopbd  31917  leoprf2  32029  opsqrlem4  32045  opsqrlem5  32046  pjbdlni  32051  pjcmul1i  32103  mptiffisupp  32589  sgncl  32729  drngidlhash  33378  evl1deg1  33518  ply1dg1rt  33521  ply1dg3rt0irred  33524  m1pmeq  33525  lvecendof1f1o  33602  fldext2rspun  33650  constrabscl  33741  zarcmplem  33844  prsssdm  33880  ordtrestNEW  33884  esumpad  34018  esumpad2  34019  esumcst  34026  esumrnmpt2  34031  sibf0  34298  sitgclcn  34308  sitgclre  34309  eulerpartlemgs2  34344  dstfrvclim1  34442  ballotlemfelz  34455  signstfveq0  34541  breprexp  34597  wevgblacfn  35069  subfacp1lem3  35142  rellysconn  35211  cvmlift2lem9  35271  nnuni  35687  ordcmp  36408  bj-snex  36996  finxpreclem4  37355  poimirlem16  37603  poimirlem17  37604  voliunnfl  37631  mbfresfi  37633  itg2addnclem2  37639  dvasin  37671  heiborlem4  37781  heiborlem6  37783  itrere  42279  sn-itrere  42449  sn-retire  42450  wepwsolem  43004  flcidc  43132  iocmbl  43175  arearect  43177  omcl3g  43296  iscard4  43495  briunov2uz  43660  eliunov2uz  43661  frege124d  43723  frege129d  43725  frege92  43917  lhe4.4ex1a  44291  dvconstbi  44296  binomcxplemnn0  44311  binomcxplemnotnn0  44318  infxr  45336  infleinflem2  45340  climneg  45581  cncfiooicc  45865  itgsinexplem1  45925  volioof  45958  stoweidlem36  46007  wallispilem3  46038  fourierdlem93  46170  fouriersw  46202  fouriercn  46203  etransclem16  46221  etransclem33  46238  sge0reuz  46418  nnfoctbdjlem  46426  hoidmvlelem3  46568  upwordnul  46851  sinnpoly  46865  dfatafv2ex  47187  sprsymrelfvlem  47464  fmtnofz04prm  47551  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  gpg3nbgrvtx0  48040  lincext2  48417  blennn0elnn  48539  itcovalsucov  48630  resccat  49036  funcf2lem2  49044  isnatd  49185  swapfelvv  49225  fucoelvv  49282  prcofelvv  49342  termco  49443  prstcprs  49522