Theorem eqeltrdi 2868

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 2860	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 2732

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

This theorem is used by:  eqeltrrdi  2869  csbexg  5267  unisn2  5269  class2set  5319  snexALT  5348  snexOLD  5407  prexOLD  5408  iotaex  6509  fvrn0  6906  f0cli  7091  funsneqopb  7149  fmptsng  7166  fmptsnd  7167  elimdelov  7509  ovima0  7593  ndmovcl  7599  caovmo  7651  soex  7918  zfrep6OLD  7952  1st2ndb  8026  fprresex  8309  smofvon2  8345  tz7.44-2  8396  oesuclem  8512  omcl  8523  oecl  8524  nnmcl  8600  nnecl  8601  fsetex  8857  fsetexb  8865  ixpexg  8929  resixpfo  8943  xpsnen  9059  ssfi  9167  cnvfi  9170  nnunifi  9261  prfi  9293  fsuppun  9357  0fsupp  9360  oiexg  9507  hartogslem1  9514  cantnfvalf  9644  rnttrcl  9701  ttrclse  9706  rankdmr1  9783  rankr1c  9803  numwdom  10062  alephon  10072  isfin5  10301  sdom2en01  10304  isf32lem9  10363  hsmexlem9  10427  iundom2g  10548  gchxpidm  10678  r1tskina  10791  tskmcl  10850  recmulnq  10973  recclnq  10975  genpelv  11009  un0mulcl  12562  znegcl  12653  zeo  12707  eqreznegel  12983  xnegcl  13265  xnn0xaddcl  13287  ioorebas  13504  modid0  13958  2txmodxeq0  13995  fzofi  14038  seqexw  14081  expcllem  14136  m1expcl2  14149  faclbnd4lem3  14359  bccl  14386  hasheq0  14427  hashrabrsn  14436  fnfz0hashnn0  14513  fnfzo0hashnn0  14516  wrdnfi  14613  cshwcl  14869  relexpaddg  15126  sgncl  15170  abs00bd  15378  iserge0  15748  sumrblem  15797  fsumcvg  15798  summolem2a  15801  sumss  15810  fsumss  15811  fsumcvg2  15813  sumsplit  15854  binom  15919  bcxmas  15924  geomulcvg  15965  prodrblem  16016  fprodcvg  16017  prodmolem2a  16021  zprod  16024  fprodntriv  16029  prodss  16034  fprodss  16035  binomfallfac  16127  bpoly1  16137  bpoly2  16143  bpoly3  16144  ruclem6  16323  smupf  16568  gcdcl  16596  lcmcl  16691  lcmfcl  16718  2mulprm  16783  pcxnn0cl  16952  pcxcl  16953  pcmptcl  16983  infpnlem2  17003  zgz  17025  4sqlem2  17041  4sqlem19  17055  vdwapval  17065  hashbc0  17097  ramcl2  17108  0ramcl  17115  ramcl  17121  isstruct2  17241  imasval  17597  imasbas  17598  imasds  17599  imasplusg  17603  imasmulr  17604  imasvsca  17606  imasip  17607  imasle  17609  qusaddvallem  17637  qusaddflem  17638  qusaddval  17639  qusaddf  17640  qusmulval  17641  qusmulf  17642  mreexexlem3d  17734  sscpwex  17904  fullresc  17940  estrres  18227  evlfcl  18310  ipopos  18624  imasmgm2  18776  qusmgm  18777  gsumress  18784  submnd0OLD  18870  qusmnd  18888  qusgrp2  19181  mulgfval  19192  issubg2  19265  triv1nsgd  19296  0subgALT  19695  torsubg  19981  frgpnabllem1  20000  lt6abl  20022  ablfaclem3  20216  ablfac2  20218  simpgnsgd  20229  qusrng  20315  srgbinomlem3  20367  ringidss  20418  qusring2  20475  isdrngd  20931  isdrngdOLD  20933  mptscmfsupp0  21111  islss3  21143  ellspsn  21187  lspprel  21278  znf1o  21764  frgpcyg  21786  cnmsgnsubg  21790  phlpropd  21868  cssval  21895  iscss  21896  dsmm0cl  21953  uvcvvcl  22000  m1detdiag  22819  m2detleiblem1  22846  pmatcollpw3fi1lem1  23011  indistopon  23226  indiscld  23316  restbas  23383  ordttopon  23418  iocpnfordt  23440  icomnfordt  23441  lecldbas  23444  fiuncmp  23629  cmpfi  23633  conncompid  23656  dissnlocfin  23755  elpt  23798  xkotop  23814  xkouni  23825  xkohaus  23879  xkoptsub  23880  imastopn  23946  filconn  24109  cfinufil  24154  alexsublem  24270  alexsub  24271  alexsubALTlem4  24276  distgp  24325  indistgp  24326  ssblps  24648  ssbl  24649  xmeter  24659  nmoi  24954  nmoeq0  24962  0nghm  24967  idnghm  24969  icccld  24992  iocmnfcld  24994  blssioo  25021  xrtgioo  25033  xrsxmet  25036  icccmp  25052  pcopt  25250  pcopt2  25251  elpi1  25273  cmetcaulem  25516  ishl2  25598  rrxmvallem  25632  ovolcl  25706  ovolunlem1a  25724  ovolunnul  25728  ovoliunnul  25735  ioombl1  25790  icombl  25792  ioombl  25793  iccmbl  25794  iccvolcl  25795  ovolioo  25796  ioovolcl  25798  ioorcl  25805  uniioovol  25807  uniioombllem2a  25810  uniioombllem4  25814  uniioombllem5  25815  vitalilem1  25836  vitalilem5  25840  mbfconstlem  25855  mbfima  25858  mbfid  25863  ismbf2d  25868  mbfss  25874  mbfmulc2lem  25875  i1fd  25909  itg1addlem2  25925  itg1addlem4  25927  itg1addlem5  25928  i1fmulc  25931  itg2l  25957  itg2cl  25960  ibl0  26014  iblrelem  26018  iblpos  26020  iblss2  26033  bddmulibl  26066  bddiblnc  26069  recnperf  26132  ply1remlem  26390  fta1glem1  26393  fta1g  26395  elply  26420  plypf1  26438  coefv0  26474  coemulc  26481  fta1  26538  elqaalem2  26552  aannenlem2  26565  aalioulem3  26570  taylfvallem1  26593  tayl0  26598  ulm0  26627  logtayl  26897  atanrecl  27148  atanbnd  27163  harmonicbnd3  27244  ftalem7  27315  basellem5  27321  ppifi  27342  sqff1o  27418  1sgmprm  27435  logexprlim  27461  dchrelbasd  27475  dchr1re  27499  lgslem4  27536  lgsne0  27571  2sqlem9  27663  2sqlem10  27664  rpvmasumlem  27723  dchrisumlem1  27725  vmalogdivsum  27775  pntrlog2bndlem5  27817  ostth  27875  lrrecse  28207  sltmuls1  28412  sltmuls2  28413  mulsuniflem  28414  noseqex  28554  n0mulscl  28610  n0fincut  28620  eln0s  28626  n0subs  28628  n0zs  28654  expscllem  28695  elz12s  28737  tgcgr4  28873  axlowdimlem16  29414  fusgrfisbase  29788  vtxdg0e  29934  rgrusgrprc  30049  wwlksnfi  30374  trlsegvdeglem7  30706  eulerpathpr  30720  0blo  31273  nmlno0lem  31274  omlsilem  31883  pjoc1i  31912  nonbooli  32132  nmlnop0iALT  32476  unopbd  32496  leoprf2  32608  opsqrlem4  32624  opsqrlem5  32625  pjbdlni  32630  pjcmul1i  32682  mptiffisupp  33165  drngidlhash  33861  evl1deg1  33986  ply1dg1rt  33990  ply1dg3rt0irred  33994  m1pmeq  33995  mplmulmvr  34049  esplyfvaln  34084  vieta  34090  lvecendof1f1o  34143  fldext2rspun  34192  constrabscl  34288  zarcmplem  34391  prsssdm  34427  ordtrestNEW  34431  esumpad  34565  esumpad2  34566  esumcst  34573  esumrnmpt2  34578  sibf0  34845  sitgclcn  34855  sitgclre  34856  eulerpartlemgs2  34891  dstfrvclim1  34989  ballotlemfelz  35002  signstfveq0  35085  breprexp  35141  r1wf  35603  fineqvnttrclselem1  35647  wevgblacfn  35708  subfacp1lem3  35761  rellysconn  35830  cvmlift2lem9  35890  nnuni  36306  ordcmp  37066  bj-snex  37779  finxpreclem4  38148  poimirlem16  38385  poimirlem17  38386  voliunnfl  38413  mbfresfi  38415  itg2addnclem2  38421  dvasin  38453  heiborlem4  38564  heiborlem6  38566  25or6to4  43072  itrere  43193  sn-itrere  43376  sn-retire  43377  wepwsolem  43883  flcidc  44011  iocmbl  44054  arearect  44056  omcl3g  44175  iscard4  44373  briunov2uz  44538  eliunov2uz  44539  frege124d  44601  frege129d  44603  frege92  44795  lhe4.4ex1a  45153  dvconstbi  45158  binomcxplemnn0  45173  binomcxplemnotnn0  45180  infxr  46196  infleinflem2  46200  climneg  46440  cncfiooicc  46722  itgsinexplem1  46782  volioof  46815  stoweidlem36  46864  wallispilem3  46895  fourierdlem93  47027  fouriersw  47059  fouriercn  47060  etransclem16  47078  etransclem33  47095  sge0reuz  47275  nnfoctbdjlem  47283  hoidmvlelem3  47425  sqrtqaa  47733  sinnpoly  47759  tmachlem-extapes  47762  tmachlem-agreefin  47776  dfatafv2ex  48101  sprsymrelfvlem  48390  fmtnofz04prm  48480  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  gpg3nbgrvtx0  48992  lincext2  49385  blennn0elnn  49507  itcovalsucov  49598  resccat  50000  funcf2lem2  50008  isnatd  50149  swapfelvv  50189  fucoelvv  50246  prcofelvv  50306  termco  50407  prstcprs  50486