Theorem eqeltrdi 2841

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eqeltrrdi  2842  csbexg  5250  unisn2  5252  class2set  5295  snexALT  5323  snex  5376  prex  5377  iotaex  6462  fvrn0  6856  f0cli  7037  funsneqopb  7091  fmptsng  7108  fmptsnd  7109  elimdelov  7448  ovima0  7531  ndmovcl  7537  caovmo  7589  soex  7857  zfrep6  7893  1st2ndb  7967  fprresex  8246  smofvon2  8282  tz7.44-2  8332  oesuclem  8446  omcl  8457  oecl  8458  nnmcl  8533  nnecl  8534  fsetex  8786  fsetexb  8794  ixpexg  8852  resixpfo  8866  xpsnen  8981  ssfi  9089  cnvfi  9092  nnunifi  9182  imafiOLD  9207  prfi  9215  fsuppun  9278  0fsupp  9281  oiexg  9428  hartogslem1  9435  cantnfvalf  9562  rnttrcl  9619  ttrclse  9624  rankdmr1  9701  rankr1c  9721  numwdom  9957  alephon  9967  isfin5  10197  sdom2en01  10200  isf32lem9  10259  hsmexlem9  10323  iundom2g  10438  gchxpidm  10567  r1tskina  10680  tskmcl  10739  recmulnq  10862  recclnq  10864  genpelv  10898  un0mulcl  12422  znegcl  12513  zeo  12565  eqreznegel  12834  xnegcl  13114  xnn0xaddcl  13136  ioorebas  13353  modid0  13803  2txmodxeq0  13840  fzofi  13883  seqexw  13926  expcllem  13981  m1expcl2  13994  faclbnd4lem3  14204  bccl  14231  hasheq0  14272  hashrabrsn  14281  fnfz0hashnn0  14357  fnfzo0hashnn0  14360  wrdnfi  14457  cshwcl  14707  relexpaddg  14962  abs00bd  15200  iserge0  15570  sumrblem  15620  fsumcvg  15621  summolem2a  15624  sumss  15633  fsumss  15634  fsumcvg2  15636  sumsplit  15677  binom  15739  bcxmas  15744  geomulcvg  15785  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  zprod  15846  fprodntriv  15851  prodss  15856  fprodss  15857  binomfallfac  15950  bpoly1  15960  bpoly2  15966  bpoly3  15967  ruclem6  16146  smupf  16391  gcdcl  16419  lcmcl  16514  lcmfcl  16541  2mulprm  16606  pcxnn0cl  16774  pcxcl  16775  pcmptcl  16805  infpnlem2  16825  zgz  16847  4sqlem2  16863  4sqlem19  16877  vdwapval  16887  hashbc0  16919  ramcl2  16930  0ramcl  16937  ramcl  16943  isstruct2  17062  imasval  17417  imasbas  17418  imasds  17419  imasplusg  17423  imasmulr  17424  imasvsca  17426  imasip  17427  imasle  17429  qusaddvallem  17457  qusaddflem  17458  qusaddval  17459  qusaddf  17460  qusmulval  17461  qusmulf  17462  mreexexlem3d  17554  sscpwex  17724  fullresc  17760  estrres  18047  evlfcl  18130  ipopos  18444  gsumress  18592  submnd0  18673  qusgrp2  18973  mulgfval  18984  issubg2  19056  triv1nsgd  19087  0subgALT  19482  torsubg  19768  frgpnabllem1  19787  lt6abl  19809  ablfaclem3  20003  ablfac2  20005  simpgnsgd  20016  qusrng  20100  srgbinomlem3  20148  ringidss  20197  qusring2  20254  isdrngd  20682  isdrngdOLD  20684  mptscmfsupp0  20862  islss3  20894  ellspsn  20938  lspprel  21030  znf1o  21490  frgpcyg  21512  cnmsgnsubg  21516  phlpropd  21594  cssval  21621  iscss  21622  dsmm0cl  21679  uvcvvcl  21726  m1detdiag  22513  m2detleiblem1  22540  pmatcollpw3fi1lem1  22702  indistopon  22917  indiscld  23007  restbas  23074  ordttopon  23109  iocpnfordt  23131  icomnfordt  23132  lecldbas  23135  fiuncmp  23320  cmpfi  23324  conncompid  23347  dissnlocfin  23445  elpt  23488  xkotop  23504  xkouni  23515  xkohaus  23569  xkoptsub  23570  imastopn  23636  filconn  23799  cfinufil  23844  alexsublem  23960  alexsub  23961  alexsubALTlem4  23966  distgp  24015  indistgp  24016  ssblps  24338  ssbl  24339  xmeter  24349  nmoi  24644  nmoeq0  24652  0nghm  24657  idnghm  24659  icccld  24682  iocmnfcld  24684  blssioo  24711  xrtgioo  24723  xrsxmet  24726  icccmp  24742  pcopt  24950  pcopt2  24951  elpi1  24973  cmetcaulem  25216  ishl2  25298  rrxmvallem  25332  ovolcl  25407  ovolunlem1a  25425  ovolunnul  25429  ovoliunnul  25436  ioombl1  25491  icombl  25493  ioombl  25494  iccmbl  25495  iccvolcl  25496  ovolioo  25497  ioovolcl  25499  ioorcl  25506  uniioovol  25508  uniioombllem2a  25511  uniioombllem4  25515  uniioombllem5  25516  vitalilem1  25537  vitalilem5  25541  mbfconstlem  25556  mbfima  25559  mbfid  25564  ismbf2d  25569  mbfss  25575  mbfmulc2lem  25576  i1fd  25610  itg1addlem2  25626  itg1addlem4  25628  itg1addlem5  25629  i1fmulc  25632  itg2l  25658  itg2cl  25661  ibl0  25716  iblrelem  25720  iblpos  25722  iblss2  25735  bddmulibl  25768  bddiblnc  25771  recnperf  25834  ply1remlem  26098  fta1glem1  26101  fta1g  26103  elply  26128  plypf1  26145  coefv0  26181  coemulc  26188  fta1  26244  elqaalem2  26256  aannenlem2  26265  aalioulem3  26270  taylfvallem1  26292  tayl0  26297  ulm0  26328  logtayl  26597  atanrecl  26849  atanbnd  26864  harmonicbnd3  26946  ftalem7  27017  basellem5  27023  ppifi  27044  sqff1o  27120  1sgmprm  27138  logexprlim  27164  dchrelbasd  27178  dchr1re  27202  lgslem4  27239  lgsne0  27274  2sqlem9  27366  2sqlem10  27367  rpvmasumlem  27426  dchrisumlem1  27428  vmalogdivsum  27478  pntrlog2bndlem5  27520  ostth  27578  lrrecse  27886  ssltmul1  28087  ssltmul2  28088  mulsuniflem  28089  noseqex  28220  n0mulscl  28274  n0sfincut  28283  eln0s  28288  n0subs  28290  n0zs  28314  expscllem  28354  elzs12  28384  tgcgr4  28510  axlowdimlem16  28937  fusgrfisbase  29308  vtxdg0e  29455  rgrusgrprc  29570  wwlksnfi  29886  trlsegvdeglem7  30208  eulerpathpr  30222  0blo  30774  nmlno0lem  30775  omlsilem  31384  pjoc1i  31413  nonbooli  31633  nmlnop0iALT  31977  unopbd  31997  leoprf2  32109  opsqrlem4  32125  opsqrlem5  32126  pjbdlni  32131  pjcmul1i  32183  mptiffisupp  32678  sgncl  32819  drngidlhash  33406  evl1deg1  33546  ply1dg1rt  33550  ply1dg3rt0irred  33553  m1pmeq  33554  mplmulmvr  33590  lvecendof1f1o  33667  fldext2rspun  33716  constrabscl  33812  zarcmplem  33915  prsssdm  33951  ordtrestNEW  33955  esumpad  34089  esumpad2  34090  esumcst  34097  esumrnmpt2  34102  sibf0  34368  sitgclcn  34378  sitgclre  34379  eulerpartlemgs2  34414  dstfrvclim1  34512  ballotlemfelz  34525  signstfveq0  34611  breprexp  34667  r1wf  35128  fineqvnttrclselem1  35162  wevgblacfn  35174  subfacp1lem3  35247  rellysconn  35316  cvmlift2lem9  35376  nnuni  35792  ordcmp  36512  bj-snex  37100  finxpreclem4  37459  poimirlem16  37696  poimirlem17  37697  voliunnfl  37724  mbfresfi  37726  itg2addnclem2  37732  dvasin  37764  heiborlem4  37874  heiborlem6  37876  itrere  42436  sn-itrere  42606  sn-retire  42607  wepwsolem  43159  flcidc  43287  iocmbl  43330  arearect  43332  omcl3g  43451  iscard4  43650  briunov2uz  43815  eliunov2uz  43816  frege124d  43878  frege129d  43880  frege92  44072  lhe4.4ex1a  44446  dvconstbi  44451  binomcxplemnn0  44466  binomcxplemnotnn0  44473  infxr  45489  infleinflem2  45493  climneg  45734  cncfiooicc  46016  itgsinexplem1  46076  volioof  46109  stoweidlem36  46158  wallispilem3  46189  fourierdlem93  46321  fouriersw  46353  fouriercn  46354  etransclem16  46372  etransclem33  46389  sge0reuz  46569  nnfoctbdjlem  46577  hoidmvlelem3  46719  sinnpoly  47015  dfatafv2ex  47337  sprsymrelfvlem  47614  fmtnofz04prm  47701  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  gpg3nbgrvtx0  48200  lincext2  48580  blennn0elnn  48702  itcovalsucov  48793  resccat  49199  funcf2lem2  49207  isnatd  49348  swapfelvv  49388  fucoelvv  49445  prcofelvv  49505  termco  49606  prstcprs  49685