Theorem eqeltrdi 2869

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  eqeltrrdi  2870  csbexg  5264  unisn2  5266  class2set  5316  snexALT  5345  snexOLD  5400  prexOLD  5401  iotaex  6515  fvrn0  6914  f0cli  7099  funsneqopb  7157  fmptsng  7174  fmptsnd  7175  elimdelov  7517  ovima0  7601  ndmovcl  7607  caovmo  7659  soex  7934  zfrep6OLD  7968  1st2ndb  8042  fprresex  8329  smofvon2  8365  tz7.44-2  8416  oesuclem  8534  omcl  8545  oecl  8546  nnmcl  8622  nnecl  8623  fsetex  8879  fsetexb  8887  ixpexg  8951  resixpfo  8965  xpsnen  9081  ssfi  9189  cnvfi  9192  nnunifi  9284  prfi  9316  fsuppun  9380  0fsupp  9383  oiexg  9530  hartogslem1  9537  cantnfvalf  9667  rnttrcl  9724  ttrclse  9729  rankdmr1  9810  rankr1c  9831  r1wf  9842  numwdom  10139  alephon  10149  isfin5  10378  sdom2en01  10381  isf32lem9  10440  hsmexlem9  10504  iundom2g  10625  gchxpidm  10755  r1tskina  10868  tskmcl  10927  recmulnq  11050  recclnq  11052  genpelv  11086  un0mulcl  12641  znegcl  12732  zeo  12786  eqreznegel  13062  xnegcl  13344  xnn0xaddcl  13366  ioorebas  13583  modid0  14038  2txmodxeq0  14075  fzofi  14118  seqexw  14161  expcllem  14216  m1expcl2  14229  faclbnd4lem3  14440  bccl  14467  hasheq0  14508  hashrabrsn  14517  fnfz0hashnn0  14594  fnfzo0hashnn0  14597  wrdnfi  14694  cshwcl  14950  relexpaddg  15207  sgncl  15251  abs00bd  15459  iserge0  15829  sumrblem  15878  fsumcvg  15879  summolem2a  15882  sumss  15891  fsumss  15892  fsumcvg2  15894  sumsplit  15935  binom  16000  bcxmas  16005  geomulcvg  16046  prodrblem  16097  fprodcvg  16098  prodmolem2a  16102  zprod  16105  fprodntriv  16110  prodss  16115  fprodss  16116  binomfallfac  16208  bpoly1  16218  bpoly2  16224  bpoly3  16225  ruclem6  16404  smupf  16649  gcdcl  16677  lcmcl  16777  lcmfcl  16804  2mulprm  16869  pcxnn0cl  17039  pcxcl  17040  pcmptcl  17070  infpnlem2  17090  zgz  17112  4sqlem2  17128  4sqlem19  17142  vdwapval  17152  hashbc0  17184  ramcl2  17195  0ramcl  17202  ramcl  17208  isstruct2  17328  imasval  17684  imasbas  17685  imasds  17686  imasplusg  17690  imasmulr  17691  imasvsca  17693  imasip  17694  imasle  17696  qusaddvallem  17724  qusaddflem  17725  qusaddval  17726  qusaddf  17727  qusmulval  17728  qusmulf  17729  mreexexlem3d  17821  sscpwex  17991  fullresc  18027  estrres  18314  evlfcl  18397  ipopos  18711  imasmgm2  18864  qusmgm  18865  gsumress  18872  submnd0OLD  18958  qusmnd  18976  qusgrp2  19269  mulgfval  19280  issubg2  19353  triv1nsgd  19384  0subgALT  19783  torsubg  20069  frgpnabllem1  20088  lt6abl  20110  ablfaclem3  20304  ablfac2  20306  simpgnsgd  20317  qusrng  20403  srgbinomlem3  20455  ringidss  20507  qusring2  20565  isdrngd  21023  isdrngdOLD  21025  mptscmfsupp0  21203  islss3  21235  ellspsn  21279  lspprel  21370  znf1o  21858  frgpcyg  21880  cnmsgnsubg  21884  phlpropd  21962  cssval  21989  iscss  21990  dsmm0cl  22047  uvcvvcl  22094  m1detdiag  22913  m2detleiblem1  22940  pmatcollpw3fi1lem1  23105  indistopon  23320  indiscld  23410  restbas  23477  ordttopon  23512  iocpnfordt  23534  icomnfordt  23535  lecldbas  23538  fiuncmp  23723  cmpfi  23727  conncompid  23750  dissnlocfin  23849  elpt  23892  xkotop  23908  xkouni  23919  xkohaus  23973  xkoptsub  23974  imastopn  24040  filconn  24203  cfinufil  24248  alexsublem  24364  alexsub  24365  alexsubALTlem4  24370  distgp  24419  indistgp  24420  ssblps  24742  ssbl  24743  xmeter  24753  nmoi  25048  nmoeq0  25056  0nghm  25061  idnghm  25063  icccld  25086  iocmnfcld  25088  blssioo  25115  xrtgioo  25127  xrsxmet  25130  icccmp  25146  pcopt  25344  pcopt2  25345  elpi1  25367  cmetcaulem  25610  ishl2  25692  rrxmvallem  25726  ovolcl  25800  ovolunlem1a  25818  ovolunnul  25822  ovoliunnul  25829  ioombl1  25884  icombl  25886  ioombl  25887  iccmbl  25888  iccvolcl  25889  ovolioo  25890  ioovolcl  25892  ioorcl  25899  uniioovol  25901  uniioombllem2a  25904  uniioombllem4  25908  uniioombllem5  25909  vitalilem1  25930  vitalilem5  25934  mbfconstlem  25949  mbfima  25952  mbfid  25957  ismbf2d  25962  mbfss  25968  mbfmulc2lem  25969  i1fd  26003  itg1addlem2  26019  itg1addlem4  26021  itg1addlem5  26022  i1fmulc  26025  itg2l  26051  itg2cl  26054  ibl0  26108  iblrelem  26112  iblpos  26114  iblss2  26127  bddmulibl  26160  bddiblnc  26163  recnperf  26226  ply1remlem  26484  fta1glem1  26487  fta1g  26489  elply  26514  plypf1  26532  coefv0  26568  coemulc  26575  fta1  26630  elqaalem2  26644  aannenlem2  26657  aalioulem3  26662  taylfvallem1  26685  tayl0  26690  ulm0  26719  logtayl  26989  atanrecl  27240  atanbnd  27255  harmonicbnd3  27336  ftalem7  27407  basellem5  27413  ppifi  27434  sqff1o  27510  1sgmprm  27527  logexprlim  27553  dchrelbasd  27567  dchr1re  27591  lgslem4  27628  lgsne0  27663  2sqlem9  27755  2sqlem10  27756  rpvmasumlem  27815  dchrisumlem1  27817  vmalogdivsum  27867  pntrlog2bndlem5  27909  ostth  27967  lrrecse  28329  sltmuls1  28534  sltmuls2  28535  mulsuniflem  28536  noseqex  28676  n0mulscl  28732  n0fincut  28742  eln0s  28748  n0subs  28750  n0zs  28776  expscllem  28817  elz12s  28859  tgcgr4  28995  axlowdimlem16  29536  fusgrfisbase  29910  vtxdg0e  30056  rgrusgrprc  30171  wwlksnfi  30496  trlsegvdeglem7  30828  eulerpathpr  30842  0blo  31395  nmlno0lem  31396  omlsilem  32005  pjoc1i  32034  nonbooli  32254  nmlnop0iALT  32598  unopbd  32618  leoprf2  32730  opsqrlem4  32746  opsqrlem5  32747  pjbdlni  32752  pjcmul1i  32804  mptiffisupp  33287  drngidlhash  33984  evl1deg1  34109  ply1dg1rt  34113  ply1dg3rt0irred  34117  m1pmeq  34118  mplmulmvr  34172  esplyfvaln  34207  vieta  34213  lvecendof1f1o  34266  fldext2rspun  34315  constrabscl  34411  zarcmplem  34514  prsssdm  34550  ordtrestNEW  34554  esumpad  34688  esumpad2  34689  esumcst  34696  esumrnmpt2  34701  sibf0  34967  sitgclcn  34977  sitgclre  34978  eulerpartlemgs2  35013  dstfrvclim1  35111  ballotlemfelz  35124  signstfveq0  35207  breprexp  35263  fineqvnttrclselem1  35790  wevgblacfn  35891  subfacp1lem3  35948  rellysconn  36017  cvmlift2lem9  36077  nnuni  36493  ordcmp  37236  bj-snex  37949  finxpreclem4  38319  poimirlem16  38556  poimirlem17  38557  voliunnfl  38584  mbfresfi  38586  itg2addnclem2  38592  dvasin  38624  heiborlem4  38750  heiborlem6  38752  25or6to4  43258  itrere  43377  sn-itrere  43554  sn-retire  43555  wepwsolem  44050  flcidc  44173  iocmbl  44216  arearect  44218  omcl3g  44337  iscard4  44535  briunov2uz  44699  eliunov2uz  44700  frege124d  44762  frege129d  44764  frege92  44956  lhe4.4ex1a  45314  dvconstbi  45319  binomcxplemnn0  45334  binomcxplemnotnn0  45341  infxr  46379  infleinflem2  46383  climneg  46623  cncfiooicc  46905  itgsinexplem1  46965  volioof  46998  stoweidlem36  47047  wallispilem3  47078  fourierdlem93  47210  fouriersw  47242  fouriercn  47243  etransclem16  47261  etransclem33  47278  sge0reuz  47458  nnfoctbdjlem  47466  hoidmvlelem3  47608  sqrtqaa  47916  sinnpoly  47942  tmachlem-extapes  47945  tmachlem-agreefin  47959  dfatafv2ex  48284  sprsymrelfvlem  48573  fmtnofz04prm  48663  nnsum4primeseven  48899  nnsum4primesevenALTV  48900  gpg3nbgrvtx0  49175  lincext2  49568  blennn0elnn  49690  itcovalsucov  49781  resccat  50183  funcf2lem2  50191  isnatd  50332  swapfelvv  50372  fucoelvv  50429  prcofelvv  50489  termco  50590  prstcprs  50669