Theorem eqeltrdi 2842

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 2834	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 2706

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

This theorem is referenced by:  eqeltrrdi  2843  csbexg  5253  unisn2  5255  class2set  5298  snexALT  5326  snex  5379  prex  5380  iotaex  6466  fvrn0  6860  f0cli  7041  funsneqopb  7095  fmptsng  7112  fmptsnd  7113  elimdelov  7452  ovima0  7535  ndmovcl  7541  caovmo  7593  soex  7861  zfrep6  7897  1st2ndb  7971  fprresex  8250  smofvon2  8286  tz7.44-2  8336  oesuclem  8450  omcl  8461  oecl  8462  nnmcl  8538  nnecl  8539  fsetex  8791  fsetexb  8799  ixpexg  8858  resixpfo  8872  xpsnen  8987  ssfi  9095  cnvfi  9098  nnunifi  9189  imafiOLD  9214  prfi  9222  fsuppun  9288  0fsupp  9291  oiexg  9438  hartogslem1  9445  cantnfvalf  9572  rnttrcl  9629  ttrclse  9634  rankdmr1  9711  rankr1c  9731  numwdom  9967  alephon  9977  isfin5  10207  sdom2en01  10210  isf32lem9  10269  hsmexlem9  10333  iundom2g  10448  gchxpidm  10578  r1tskina  10691  tskmcl  10750  recmulnq  10873  recclnq  10875  genpelv  10909  un0mulcl  12433  znegcl  12524  zeo  12576  eqreznegel  12845  xnegcl  13126  xnn0xaddcl  13148  ioorebas  13365  modid0  13815  2txmodxeq0  13852  fzofi  13895  seqexw  13938  expcllem  13993  m1expcl2  14006  faclbnd4lem3  14216  bccl  14243  hasheq0  14284  hashrabrsn  14293  fnfz0hashnn0  14369  fnfzo0hashnn0  14372  wrdnfi  14469  cshwcl  14719  relexpaddg  14974  abs00bd  15212  iserge0  15582  sumrblem  15632  fsumcvg  15633  summolem2a  15636  sumss  15645  fsumss  15646  fsumcvg2  15648  sumsplit  15689  binom  15751  bcxmas  15756  geomulcvg  15797  prodrblem  15850  fprodcvg  15851  prodmolem2a  15855  zprod  15858  fprodntriv  15863  prodss  15868  fprodss  15869  binomfallfac  15962  bpoly1  15972  bpoly2  15978  bpoly3  15979  ruclem6  16158  smupf  16403  gcdcl  16431  lcmcl  16526  lcmfcl  16553  2mulprm  16618  pcxnn0cl  16786  pcxcl  16787  pcmptcl  16817  infpnlem2  16837  zgz  16859  4sqlem2  16875  4sqlem19  16889  vdwapval  16899  hashbc0  16931  ramcl2  16942  0ramcl  16949  ramcl  16955  isstruct2  17074  imasval  17430  imasbas  17431  imasds  17432  imasplusg  17436  imasmulr  17437  imasvsca  17439  imasip  17440  imasle  17442  qusaddvallem  17470  qusaddflem  17471  qusaddval  17472  qusaddf  17473  qusmulval  17474  qusmulf  17475  mreexexlem3d  17567  sscpwex  17737  fullresc  17773  estrres  18060  evlfcl  18143  ipopos  18457  gsumress  18605  submnd0  18686  qusgrp2  18986  mulgfval  18997  issubg2  19069  triv1nsgd  19100  0subgALT  19495  torsubg  19781  frgpnabllem1  19800  lt6abl  19822  ablfaclem3  20016  ablfac2  20018  simpgnsgd  20029  qusrng  20113  srgbinomlem3  20161  ringidss  20210  qusring2  20268  isdrngd  20696  isdrngdOLD  20698  mptscmfsupp0  20876  islss3  20908  ellspsn  20952  lspprel  21044  znf1o  21504  frgpcyg  21526  cnmsgnsubg  21530  phlpropd  21608  cssval  21635  iscss  21636  dsmm0cl  21693  uvcvvcl  21740  m1detdiag  22539  m2detleiblem1  22566  pmatcollpw3fi1lem1  22728  indistopon  22943  indiscld  23033  restbas  23100  ordttopon  23135  iocpnfordt  23157  icomnfordt  23158  lecldbas  23161  fiuncmp  23346  cmpfi  23350  conncompid  23373  dissnlocfin  23471  elpt  23514  xkotop  23530  xkouni  23541  xkohaus  23595  xkoptsub  23596  imastopn  23662  filconn  23825  cfinufil  23870  alexsublem  23986  alexsub  23987  alexsubALTlem4  23992  distgp  24041  indistgp  24042  ssblps  24364  ssbl  24365  xmeter  24375  nmoi  24670  nmoeq0  24678  0nghm  24683  idnghm  24685  icccld  24708  iocmnfcld  24710  blssioo  24737  xrtgioo  24749  xrsxmet  24752  icccmp  24768  pcopt  24976  pcopt2  24977  elpi1  24999  cmetcaulem  25242  ishl2  25324  rrxmvallem  25358  ovolcl  25433  ovolunlem1a  25451  ovolunnul  25455  ovoliunnul  25462  ioombl1  25517  icombl  25519  ioombl  25520  iccmbl  25521  iccvolcl  25522  ovolioo  25523  ioovolcl  25525  ioorcl  25532  uniioovol  25534  uniioombllem2a  25537  uniioombllem4  25541  uniioombllem5  25542  vitalilem1  25563  vitalilem5  25567  mbfconstlem  25582  mbfima  25585  mbfid  25590  ismbf2d  25595  mbfss  25601  mbfmulc2lem  25602  i1fd  25636  itg1addlem2  25652  itg1addlem4  25654  itg1addlem5  25655  i1fmulc  25658  itg2l  25684  itg2cl  25687  ibl0  25742  iblrelem  25746  iblpos  25748  iblss2  25761  bddmulibl  25794  bddiblnc  25797  recnperf  25860  ply1remlem  26124  fta1glem1  26127  fta1g  26129  elply  26154  plypf1  26171  coefv0  26207  coemulc  26214  fta1  26270  elqaalem2  26282  aannenlem2  26291  aalioulem3  26296  taylfvallem1  26318  tayl0  26323  ulm0  26354  logtayl  26623  atanrecl  26875  atanbnd  26890  harmonicbnd3  26972  ftalem7  27043  basellem5  27049  ppifi  27070  sqff1o  27146  1sgmprm  27164  logexprlim  27190  dchrelbasd  27204  dchr1re  27228  lgslem4  27265  lgsne0  27300  2sqlem9  27392  2sqlem10  27393  rpvmasumlem  27452  dchrisumlem1  27454  vmalogdivsum  27504  pntrlog2bndlem5  27546  ostth  27604  lrrecse  27912  ssltmul1  28116  ssltmul2  28117  mulsuniflem  28118  noseqex  28250  n0mulscl  28305  n0sfincut  28315  eln0s  28320  n0subs  28322  n0zs  28347  expscllem  28388  elzs12  28421  tgcgr4  28552  axlowdimlem16  28979  fusgrfisbase  29350  vtxdg0e  29497  rgrusgrprc  29612  wwlksnfi  29928  trlsegvdeglem7  30250  eulerpathpr  30264  0blo  30816  nmlno0lem  30817  omlsilem  31426  pjoc1i  31455  nonbooli  31675  nmlnop0iALT  32019  unopbd  32039  leoprf2  32151  opsqrlem4  32167  opsqrlem5  32168  pjbdlni  32173  pjcmul1i  32225  mptiffisupp  32721  sgncl  32861  drngidlhash  33464  evl1deg1  33606  ply1dg1rt  33610  ply1dg3rt0irred  33614  m1pmeq  33615  mplmulmvr  33653  vieta  33685  lvecendof1f1o  33739  fldext2rspun  33788  constrabscl  33884  zarcmplem  33987  prsssdm  34023  ordtrestNEW  34027  esumpad  34161  esumpad2  34162  esumcst  34169  esumrnmpt2  34174  sibf0  34440  sitgclcn  34450  sitgclre  34451  eulerpartlemgs2  34486  dstfrvclim1  34584  ballotlemfelz  34597  signstfveq0  34683  breprexp  34739  r1wf  35201  fineqvnttrclselem1  35226  wevgblacfn  35252  subfacp1lem3  35325  rellysconn  35394  cvmlift2lem9  35454  nnuni  35870  ordcmp  36590  bj-snex  37179  finxpreclem4  37538  poimirlem16  37776  poimirlem17  37777  voliunnfl  37804  mbfresfi  37806  itg2addnclem2  37812  dvasin  37844  heiborlem4  37954  heiborlem6  37956  itrere  42515  sn-itrere  42685  sn-retire  42686  wepwsolem  43226  flcidc  43354  iocmbl  43397  arearect  43399  omcl3g  43518  iscard4  43716  briunov2uz  43881  eliunov2uz  43882  frege124d  43944  frege129d  43946  frege92  44138  lhe4.4ex1a  44512  dvconstbi  44517  binomcxplemnn0  44532  binomcxplemnotnn0  44539  infxr  45553  infleinflem2  45557  climneg  45798  cncfiooicc  46080  itgsinexplem1  46140  volioof  46173  stoweidlem36  46222  wallispilem3  46253  fourierdlem93  46385  fouriersw  46417  fouriercn  46418  etransclem16  46436  etransclem33  46453  sge0reuz  46633  nnfoctbdjlem  46641  hoidmvlelem3  46783  sinnpoly  47079  dfatafv2ex  47401  sprsymrelfvlem  47678  fmtnofz04prm  47765  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  gpg3nbgrvtx0  48264  lincext2  48643  blennn0elnn  48765  itcovalsucov  48856  resccat  49261  funcf2lem2  49269  isnatd  49410  swapfelvv  49450  fucoelvv  49507  prcofelvv  49567  termco  49668  prstcprs  49747