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  6513  fvrn0  6911  f0cli  7096  funsneqopb  7154  fmptsng  7171  fmptsnd  7172  elimdelov  7514  ovima0  7598  ndmovcl  7604  caovmo  7656  soex  7931  zfrep6OLD  7965  1st2ndb  8039  fprresex  8321  smofvon2  8357  tz7.44-2  8408  oesuclem  8526  omcl  8537  oecl  8538  nnmcl  8614  nnecl  8615  fsetex  8871  fsetexb  8879  ixpexg  8943  resixpfo  8957  xpsnen  9073  ssfi  9181  cnvfi  9184  nnunifi  9276  prfi  9308  fsuppun  9372  0fsupp  9375  oiexg  9522  hartogslem1  9529  cantnfvalf  9659  rnttrcl  9716  ttrclse  9721  rankdmr1  9802  rankr1c  9823  r1wf  9834  numwdom  10131  alephon  10141  isfin5  10370  sdom2en01  10373  isf32lem9  10432  hsmexlem9  10496  iundom2g  10617  gchxpidm  10747  r1tskina  10860  tskmcl  10919  recmulnq  11042  recclnq  11044  genpelv  11078  un0mulcl  12633  znegcl  12724  zeo  12778  eqreznegel  13054  xnegcl  13336  xnn0xaddcl  13358  ioorebas  13575  modid0  14030  2txmodxeq0  14067  fzofi  14110  seqexw  14153  expcllem  14208  m1expcl2  14221  faclbnd4lem3  14432  bccl  14459  hasheq0  14500  hashrabrsn  14509  fnfz0hashnn0  14586  fnfzo0hashnn0  14589  wrdnfi  14686  cshwcl  14942  relexpaddg  15199  sgncl  15243  abs00bd  15451  iserge0  15821  sumrblem  15870  fsumcvg  15871  summolem2a  15874  sumss  15883  fsumss  15884  fsumcvg2  15886  sumsplit  15927  binom  15992  bcxmas  15997  geomulcvg  16038  prodrblem  16089  fprodcvg  16090  prodmolem2a  16094  zprod  16097  fprodntriv  16102  prodss  16107  fprodss  16108  binomfallfac  16200  bpoly1  16210  bpoly2  16216  bpoly3  16217  ruclem6  16396  smupf  16641  gcdcl  16669  lcmcl  16769  lcmfcl  16796  2mulprm  16861  pcxnn0cl  17031  pcxcl  17032  pcmptcl  17062  infpnlem2  17082  zgz  17104  4sqlem2  17120  4sqlem19  17134  vdwapval  17144  hashbc0  17176  ramcl2  17187  0ramcl  17194  ramcl  17200  isstruct2  17320  imasval  17676  imasbas  17677  imasds  17678  imasplusg  17682  imasmulr  17683  imasvsca  17685  imasip  17686  imasle  17688  qusaddvallem  17716  qusaddflem  17717  qusaddval  17718  qusaddf  17719  qusmulval  17720  qusmulf  17721  mreexexlem3d  17813  sscpwex  17983  fullresc  18019  estrres  18306  evlfcl  18389  ipopos  18703  imasmgm2  18856  qusmgm  18857  gsumress  18864  submnd0OLD  18950  qusmnd  18968  qusgrp2  19261  mulgfval  19272  issubg2  19345  triv1nsgd  19376  0subgALT  19775  torsubg  20061  frgpnabllem1  20080  lt6abl  20102  ablfaclem3  20296  ablfac2  20298  simpgnsgd  20309  qusrng  20395  srgbinomlem3  20447  ringidss  20499  qusring2  20557  isdrngd  21015  isdrngdOLD  21017  mptscmfsupp0  21195  islss3  21227  ellspsn  21271  lspprel  21362  znf1o  21850  frgpcyg  21872  cnmsgnsubg  21876  phlpropd  21954  cssval  21981  iscss  21982  dsmm0cl  22039  uvcvvcl  22086  m1detdiag  22905  m2detleiblem1  22932  pmatcollpw3fi1lem1  23097  indistopon  23312  indiscld  23402  restbas  23469  ordttopon  23504  iocpnfordt  23526  icomnfordt  23527  lecldbas  23530  fiuncmp  23715  cmpfi  23719  conncompid  23742  dissnlocfin  23841  elpt  23884  xkotop  23900  xkouni  23911  xkohaus  23965  xkoptsub  23966  imastopn  24032  filconn  24195  cfinufil  24240  alexsublem  24356  alexsub  24357  alexsubALTlem4  24362  distgp  24411  indistgp  24412  ssblps  24734  ssbl  24735  xmeter  24745  nmoi  25040  nmoeq0  25048  0nghm  25053  idnghm  25055  icccld  25078  iocmnfcld  25080  blssioo  25107  xrtgioo  25119  xrsxmet  25122  icccmp  25138  pcopt  25336  pcopt2  25337  elpi1  25359  cmetcaulem  25602  ishl2  25684  rrxmvallem  25718  ovolcl  25792  ovolunlem1a  25810  ovolunnul  25814  ovoliunnul  25821  ioombl1  25876  icombl  25878  ioombl  25879  iccmbl  25880  iccvolcl  25881  ovolioo  25882  ioovolcl  25884  ioorcl  25891  uniioovol  25893  uniioombllem2a  25896  uniioombllem4  25900  uniioombllem5  25901  vitalilem1  25922  vitalilem5  25926  mbfconstlem  25941  mbfima  25944  mbfid  25949  ismbf2d  25954  mbfss  25960  mbfmulc2lem  25961  i1fd  25995  itg1addlem2  26011  itg1addlem4  26013  itg1addlem5  26014  i1fmulc  26017  itg2l  26043  itg2cl  26046  ibl0  26100  iblrelem  26104  iblpos  26106  iblss2  26119  bddmulibl  26152  bddiblnc  26155  recnperf  26218  ply1remlem  26476  fta1glem1  26479  fta1g  26481  elply  26506  plypf1  26524  coefv0  26560  coemulc  26567  fta1  26622  elqaalem2  26636  aannenlem2  26649  aalioulem3  26654  taylfvallem1  26677  tayl0  26682  ulm0  26711  logtayl  26981  atanrecl  27232  atanbnd  27247  harmonicbnd3  27328  ftalem7  27399  basellem5  27405  ppifi  27426  sqff1o  27502  1sgmprm  27519  logexprlim  27545  dchrelbasd  27559  dchr1re  27583  lgslem4  27620  lgsne0  27655  2sqlem9  27747  2sqlem10  27748  rpvmasumlem  27807  dchrisumlem1  27809  vmalogdivsum  27859  pntrlog2bndlem5  27901  ostth  27959  lrrecse  28321  sltmuls1  28526  sltmuls2  28527  mulsuniflem  28528  noseqex  28668  n0mulscl  28724  n0fincut  28734  eln0s  28740  n0subs  28742  n0zs  28768  expscllem  28809  elz12s  28851  tgcgr4  28987  axlowdimlem16  29528  fusgrfisbase  29902  vtxdg0e  30048  rgrusgrprc  30163  wwlksnfi  30488  trlsegvdeglem7  30820  eulerpathpr  30834  0blo  31387  nmlno0lem  31388  omlsilem  31997  pjoc1i  32026  nonbooli  32246  nmlnop0iALT  32590  unopbd  32610  leoprf2  32722  opsqrlem4  32738  opsqrlem5  32739  pjbdlni  32744  pjcmul1i  32796  mptiffisupp  33279  drngidlhash  33976  evl1deg1  34101  ply1dg1rt  34105  ply1dg3rt0irred  34109  m1pmeq  34110  mplmulmvr  34164  esplyfvaln  34199  vieta  34205  lvecendof1f1o  34258  fldext2rspun  34307  constrabscl  34403  zarcmplem  34506  prsssdm  34542  ordtrestNEW  34546  esumpad  34680  esumpad2  34681  esumcst  34688  esumrnmpt2  34693  sibf0  34959  sitgclcn  34969  sitgclre  34970  eulerpartlemgs2  35005  dstfrvclim1  35103  ballotlemfelz  35116  signstfveq0  35199  breprexp  35255  fineqvnttrclselem1  35772  wevgblacfn  35873  subfacp1lem3  35926  rellysconn  35995  cvmlift2lem9  36055  nnuni  36471  ordcmp  37215  bj-snex  37928  finxpreclem4  38297  poimirlem16  38534  poimirlem17  38535  voliunnfl  38562  mbfresfi  38564  itg2addnclem2  38570  dvasin  38602  heiborlem4  38728  heiborlem6  38730  25or6to4  43236  itrere  43355  sn-itrere  43532  sn-retire  43533  wepwsolem  44028  flcidc  44156  iocmbl  44199  arearect  44201  omcl3g  44320  iscard4  44518  briunov2uz  44683  eliunov2uz  44684  frege124d  44746  frege129d  44748  frege92  44940  lhe4.4ex1a  45298  dvconstbi  45303  binomcxplemnn0  45318  binomcxplemnotnn0  45325  infxr  46347  infleinflem2  46351  climneg  46591  cncfiooicc  46873  itgsinexplem1  46933  volioof  46966  stoweidlem36  47015  wallispilem3  47046  fourierdlem93  47178  fouriersw  47210  fouriercn  47211  etransclem16  47229  etransclem33  47246  sge0reuz  47426  nnfoctbdjlem  47434  hoidmvlelem3  47576  sqrtqaa  47884  sinnpoly  47910  tmachlem-extapes  47913  tmachlem-agreefin  47927  dfatafv2ex  48252  sprsymrelfvlem  48541  fmtnofz04prm  48631  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  gpg3nbgrvtx0  49143  lincext2  49536  blennn0elnn  49658  itcovalsucov  49749  resccat  50151  funcf2lem2  50159  isnatd  50300  swapfelvv  50340  fucoelvv  50397  prcofelvv  50457  termco  50558  prstcprs  50637