Theorem eqeltrdi 2852

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eqeltrrdi  2853  csbexg  5328  unisn2  5330  class2set  5373  snexALT  5401  snex  5451  prex  5452  iotaex  6546  iotaexOLD  6553  fvrn0  6950  f0cli  7132  funsneqopb  7186  fmptsng  7202  fmptsnd  7203  elimdelov  7546  ovima0  7629  ndmovcl  7635  caovmo  7687  soex  7961  zfrep6  7995  1st2ndb  8070  fprresex  8351  wfrlem17OLD  8381  smofvon2  8412  tz7.44-2  8463  oesuclem  8581  omcl  8592  oecl  8593  nnmcl  8668  nnecl  8669  fsetex  8914  fsetexb  8922  ixpexg  8980  resixpfo  8994  en1bOLD  9089  xpsnen  9121  ssfi  9240  cnvfi  9243  nnunifi  9355  imafiOLD  9382  xpfiOLD  9387  prfi  9391  fsuppun  9456  0fsupp  9459  oiexg  9604  hartogslem1  9611  cantnfvalf  9734  rnttrcl  9791  ttrclse  9796  rankdmr1  9870  rankr1c  9890  numwdom  10128  alephon  10138  isfin5  10368  sdom2en01  10371  isf32lem9  10430  hsmexlem9  10494  iundom2g  10609  gchxpidm  10738  r1tskina  10851  tskmcl  10910  recmulnq  11033  recclnq  11035  genpelv  11069  un0mulcl  12587  znegcl  12678  zeo  12729  eqreznegel  12999  xnegcl  13275  xnn0xaddcl  13297  ioorebas  13511  modid0  13948  2txmodxeq0  13982  fzofi  14025  seqexw  14068  expcllem  14123  m1expcl2  14136  faclbnd4lem3  14344  bccl  14371  hasheq0  14412  hashrabrsn  14421  fnfz0hashnn0  14497  fnfzo0hashnn0  14500  wrdnfi  14596  cshwcl  14846  relexpaddg  15102  abs00bd  15340  iserge0  15709  sumrblem  15759  fsumcvg  15760  summolem2a  15763  sumss  15772  fsumss  15773  fsumcvg2  15775  sumsplit  15816  binom  15878  bcxmas  15883  geomulcvg  15924  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  fprodntriv  15990  prodss  15995  fprodss  15996  binomfallfac  16089  bpoly1  16099  bpoly2  16105  bpoly3  16106  ruclem6  16283  smupf  16524  gcdcl  16552  lcmcl  16648  lcmfcl  16675  2mulprm  16740  pcxnn0cl  16907  pcxcl  16908  pcmptcl  16938  infpnlem2  16958  zgz  16980  4sqlem2  16996  4sqlem19  17010  vdwapval  17020  hashbc0  17052  ramcl2  17063  0ramcl  17070  ramcl  17076  isstruct2  17196  imasval  17571  imasbas  17572  imasds  17573  imasplusg  17577  imasmulr  17578  imasvsca  17580  imasip  17581  imasle  17583  qusaddvallem  17611  qusaddflem  17612  qusaddval  17613  qusaddf  17614  qusmulval  17615  qusmulf  17616  mreexexlem3d  17704  sscpwex  17876  fullresc  17915  estrres  18208  evlfcl  18292  ipopos  18606  gsumress  18720  submnd0  18801  qusgrp2  19098  mulgfval  19109  issubg2  19181  triv1nsgd  19213  0subgALT  19610  torsubg  19896  frgpnabllem1  19915  lt6abl  19937  ablfaclem3  20131  ablfac2  20133  simpgnsgd  20144  qusrng  20207  srgbinomlem3  20255  ringidss  20300  qusring2  20357  isdrngd  20787  isdrngdOLD  20789  mptscmfsupp0  20947  islss3  20980  ellspsn  21024  lspprel  21116  znf1o  21593  frgpcyg  21615  cnmsgnsubg  21618  phlpropd  21696  cssval  21723  iscss  21724  dsmm0cl  21783  uvcvvcl  21830  m1detdiag  22624  m2detleiblem1  22651  pmatcollpw3fi1lem1  22813  indistopon  23029  indiscld  23120  restbas  23187  ordttopon  23222  iocpnfordt  23244  icomnfordt  23245  lecldbas  23248  fiuncmp  23433  cmpfi  23437  conncompid  23460  dissnlocfin  23558  elpt  23601  xkotop  23617  xkouni  23628  xkohaus  23682  xkoptsub  23683  imastopn  23749  filconn  23912  cfinufil  23957  alexsublem  24073  alexsub  24074  alexsubALTlem4  24079  distgp  24128  indistgp  24129  ssblps  24453  ssbl  24454  xmeter  24464  nmoi  24770  nmoeq0  24778  0nghm  24783  idnghm  24785  icccld  24808  iocmnfcld  24810  blssioo  24836  xrtgioo  24847  xrsxmet  24850  icccmp  24866  pcopt  25074  pcopt2  25075  elpi1  25097  cmetcaulem  25341  ishl2  25423  rrxmvallem  25457  ovolcl  25532  ovolunlem1a  25550  ovolunnul  25554  ovoliunnul  25561  ioombl1  25616  icombl  25618  ioombl  25619  iccmbl  25620  iccvolcl  25621  ovolioo  25622  ioovolcl  25624  ioorcl  25631  uniioovol  25633  uniioombllem2a  25636  uniioombllem4  25640  uniioombllem5  25641  vitalilem1  25662  vitalilem5  25666  mbfconstlem  25681  mbfima  25684  mbfid  25689  ismbf2d  25694  mbfss  25700  mbfmulc2lem  25701  i1fd  25735  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  i1fmulc  25758  itg2l  25784  itg2cl  25787  ibl0  25842  iblrelem  25846  iblpos  25848  iblss2  25861  bddmulibl  25894  bddiblnc  25897  recnperf  25960  ply1remlem  26224  fta1glem1  26227  fta1g  26229  elply  26254  plypf1  26271  coefv0  26307  coemulc  26314  fta1  26368  elqaalem2  26380  aannenlem2  26389  aalioulem3  26394  taylfvallem1  26416  tayl0  26421  ulm0  26452  logtayl  26720  atanrecl  26972  atanbnd  26987  harmonicbnd3  27069  ftalem7  27140  basellem5  27146  ppifi  27167  sqff1o  27243  1sgmprm  27261  logexprlim  27287  dchrelbasd  27301  dchr1re  27325  lgslem4  27362  lgsne0  27397  2sqlem9  27489  2sqlem10  27490  rpvmasumlem  27549  dchrisumlem1  27551  vmalogdivsum  27601  pntrlog2bndlem5  27643  ostth  27701  lrrecse  27993  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  noseqex  28313  n0mulscl  28366  eln0s  28376  n0subs  28378  n0zs  28393  expscl  28431  elzs12  28439  tgcgr4  28557  axlowdimlem16  28990  fusgrfisbase  29363  vtxdg0e  29510  rgrusgrprc  29625  wwlksnfi  29939  trlsegvdeglem7  30258  eulerpathpr  30272  0blo  30824  nmlno0lem  30825  omlsilem  31434  pjoc1i  31463  nonbooli  31683  nmlnop0iALT  32027  unopbd  32047  leoprf2  32159  opsqrlem4  32175  opsqrlem5  32176  pjbdlni  32181  pjcmul1i  32233  mptiffisupp  32705  drngidlhash  33427  evl1deg1  33566  ply1dg1rt  33569  ply1dg3rt0irred  33572  m1pmeq  33573  lvecendof1f1o  33646  zarcmplem  33827  prsssdm  33863  ordtrestNEW  33867  esumpad  34019  esumpad2  34020  esumcst  34027  esumrnmpt2  34032  sibf0  34299  sitgclcn  34309  sitgclre  34310  eulerpartlemgs2  34345  dstfrvclim1  34442  ballotlemfelz  34455  sgncl  34503  signstfveq0  34554  breprexp  34610  wevgblacfn  35076  subfacp1lem3  35150  rellysconn  35219  cvmlift2lem9  35279  nnuni  35689  ordcmp  36413  bj-snex  37001  finxpreclem4  37360  poimirlem16  37596  poimirlem17  37597  voliunnfl  37624  mbfresfi  37626  itg2addnclem2  37632  dvasin  37664  heiborlem4  37774  heiborlem6  37776  itrere  42307  sn-itrere  42444  sn-retire  42445  wepwsolem  42999  flcidc  43131  iocmbl  43174  arearect  43176  omcl3g  43296  iscard4  43495  briunov2uz  43660  eliunov2uz  43661  frege124d  43723  frege129d  43725  frege92  43917  lhe4.4ex1a  44298  dvconstbi  44303  binomcxplemnn0  44318  binomcxplemnotnn0  44325  infxr  45282  infleinflem2  45286  climneg  45531  cncfiooicc  45815  itgsinexplem1  45875  volioof  45908  stoweidlem36  45957  wallispilem3  45988  fourierdlem93  46120  fouriersw  46152  fouriercn  46153  etransclem16  46171  etransclem33  46188  sge0reuz  46368  nnfoctbdjlem  46376  hoidmvlelem3  46518  upwordnul  46799  dfatafv2ex  47128  sprsymrelfvlem  47364  fmtnofz04prm  47451  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  lincext2  48184  blennn0elnn  48311  itcovalsucov  48402  prstcprs  48742