Theorem eqeltrdi 2845

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqeltrrdi  2846  csbexg  5257  unisn2  5259  class2set  5302  snexALT  5330  snexOLD  5388  prexOLD  5389  iotaex  6476  fvrn0  6870  f0cli  7052  funsneqopb  7107  fmptsng  7124  fmptsnd  7125  elimdelov  7464  ovima0  7547  ndmovcl  7553  caovmo  7605  soex  7873  zfrep6  7909  1st2ndb  7983  fprresex  8262  smofvon2  8298  tz7.44-2  8348  oesuclem  8462  omcl  8473  oecl  8474  nnmcl  8550  nnecl  8551  fsetex  8805  fsetexb  8813  ixpexg  8872  resixpfo  8886  xpsnen  9001  ssfi  9109  cnvfi  9112  nnunifi  9203  imafiOLD  9228  prfi  9236  fsuppun  9302  0fsupp  9305  oiexg  9452  hartogslem1  9459  cantnfvalf  9586  rnttrcl  9643  ttrclse  9648  rankdmr1  9725  rankr1c  9745  numwdom  9981  alephon  9991  isfin5  10221  sdom2en01  10224  isf32lem9  10283  hsmexlem9  10347  iundom2g  10462  gchxpidm  10592  r1tskina  10705  tskmcl  10764  recmulnq  10887  recclnq  10889  genpelv  10923  un0mulcl  12447  znegcl  12538  zeo  12590  eqreznegel  12859  xnegcl  13140  xnn0xaddcl  13162  ioorebas  13379  modid0  13829  2txmodxeq0  13866  fzofi  13909  seqexw  13952  expcllem  14007  m1expcl2  14020  faclbnd4lem3  14230  bccl  14257  hasheq0  14298  hashrabrsn  14307  fnfz0hashnn0  14383  fnfzo0hashnn0  14386  wrdnfi  14483  cshwcl  14733  relexpaddg  14988  abs00bd  15226  iserge0  15596  sumrblem  15646  fsumcvg  15647  summolem2a  15650  sumss  15659  fsumss  15660  fsumcvg2  15662  sumsplit  15703  binom  15765  bcxmas  15770  geomulcvg  15811  prodrblem  15864  fprodcvg  15865  prodmolem2a  15869  zprod  15872  fprodntriv  15877  prodss  15882  fprodss  15883  binomfallfac  15976  bpoly1  15986  bpoly2  15992  bpoly3  15993  ruclem6  16172  smupf  16417  gcdcl  16445  lcmcl  16540  lcmfcl  16567  2mulprm  16632  pcxnn0cl  16800  pcxcl  16801  pcmptcl  16831  infpnlem2  16851  zgz  16873  4sqlem2  16889  4sqlem19  16903  vdwapval  16913  hashbc0  16945  ramcl2  16956  0ramcl  16963  ramcl  16969  isstruct2  17088  imasval  17444  imasbas  17445  imasds  17446  imasplusg  17450  imasmulr  17451  imasvsca  17453  imasip  17454  imasle  17456  qusaddvallem  17484  qusaddflem  17485  qusaddval  17486  qusaddf  17487  qusmulval  17488  qusmulf  17489  mreexexlem3d  17581  sscpwex  17751  fullresc  17787  estrres  18074  evlfcl  18157  ipopos  18471  gsumress  18619  submnd0  18700  qusgrp2  19000  mulgfval  19011  issubg2  19083  triv1nsgd  19114  0subgALT  19509  torsubg  19795  frgpnabllem1  19814  lt6abl  19836  ablfaclem3  20030  ablfac2  20032  simpgnsgd  20043  qusrng  20127  srgbinomlem3  20175  ringidss  20224  qusring2  20282  isdrngd  20710  isdrngdOLD  20712  mptscmfsupp0  20890  islss3  20922  ellspsn  20966  lspprel  21058  znf1o  21518  frgpcyg  21540  cnmsgnsubg  21544  phlpropd  21622  cssval  21649  iscss  21650  dsmm0cl  21707  uvcvvcl  21754  m1detdiag  22553  m2detleiblem1  22580  pmatcollpw3fi1lem1  22742  indistopon  22957  indiscld  23047  restbas  23114  ordttopon  23149  iocpnfordt  23171  icomnfordt  23172  lecldbas  23175  fiuncmp  23360  cmpfi  23364  conncompid  23387  dissnlocfin  23485  elpt  23528  xkotop  23544  xkouni  23555  xkohaus  23609  xkoptsub  23610  imastopn  23676  filconn  23839  cfinufil  23884  alexsublem  24000  alexsub  24001  alexsubALTlem4  24006  distgp  24055  indistgp  24056  ssblps  24378  ssbl  24379  xmeter  24389  nmoi  24684  nmoeq0  24692  0nghm  24697  idnghm  24699  icccld  24722  iocmnfcld  24724  blssioo  24751  xrtgioo  24763  xrsxmet  24766  icccmp  24782  pcopt  24990  pcopt2  24991  elpi1  25013  cmetcaulem  25256  ishl2  25338  rrxmvallem  25372  ovolcl  25447  ovolunlem1a  25465  ovolunnul  25469  ovoliunnul  25476  ioombl1  25531  icombl  25533  ioombl  25534  iccmbl  25535  iccvolcl  25536  ovolioo  25537  ioovolcl  25539  ioorcl  25546  uniioovol  25548  uniioombllem2a  25551  uniioombllem4  25555  uniioombllem5  25556  vitalilem1  25577  vitalilem5  25581  mbfconstlem  25596  mbfima  25599  mbfid  25604  ismbf2d  25609  mbfss  25615  mbfmulc2lem  25616  i1fd  25650  itg1addlem2  25666  itg1addlem4  25668  itg1addlem5  25669  i1fmulc  25672  itg2l  25698  itg2cl  25701  ibl0  25756  iblrelem  25760  iblpos  25762  iblss2  25775  bddmulibl  25808  bddiblnc  25811  recnperf  25874  ply1remlem  26138  fta1glem1  26141  fta1g  26143  elply  26168  plypf1  26185  coefv0  26221  coemulc  26228  fta1  26284  elqaalem2  26296  aannenlem2  26305  aalioulem3  26310  taylfvallem1  26332  tayl0  26337  ulm0  26368  logtayl  26637  atanrecl  26889  atanbnd  26904  harmonicbnd3  26986  ftalem7  27057  basellem5  27063  ppifi  27084  sqff1o  27160  1sgmprm  27178  logexprlim  27204  dchrelbasd  27218  dchr1re  27242  lgslem4  27279  lgsne0  27314  2sqlem9  27406  2sqlem10  27407  rpvmasumlem  27466  dchrisumlem1  27468  vmalogdivsum  27518  pntrlog2bndlem5  27560  ostth  27618  lrrecse  27950  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  noseqex  28297  n0mulscl  28353  n0fincut  28363  eln0s  28369  n0subs  28371  n0zs  28397  expscllem  28438  elz12s  28480  tgcgr4  28615  axlowdimlem16  29042  fusgrfisbase  29413  vtxdg0e  29560  rgrusgrprc  29675  wwlksnfi  29991  trlsegvdeglem7  30313  eulerpathpr  30327  0blo  30880  nmlno0lem  30881  omlsilem  31490  pjoc1i  31519  nonbooli  31739  nmlnop0iALT  32083  unopbd  32103  leoprf2  32215  opsqrlem4  32231  opsqrlem5  32232  pjbdlni  32237  pjcmul1i  32289  mptiffisupp  32783  sgncl  32923  drngidlhash  33527  evl1deg1  33669  ply1dg1rt  33673  ply1dg3rt0irred  33677  m1pmeq  33678  mplmulmvr  33716  esplyfvaln  33751  vieta  33757  lvecendof1f1o  33811  fldext2rspun  33860  constrabscl  33956  zarcmplem  34059  prsssdm  34095  ordtrestNEW  34099  esumpad  34233  esumpad2  34234  esumcst  34241  esumrnmpt2  34246  sibf0  34512  sitgclcn  34522  sitgclre  34523  eulerpartlemgs2  34558  dstfrvclim1  34656  ballotlemfelz  34669  signstfveq0  34755  breprexp  34811  r1wf  35273  fineqvnttrclselem1  35299  wevgblacfn  35325  subfacp1lem3  35398  rellysconn  35467  cvmlift2lem9  35527  nnuni  35943  ordcmp  36663  bj-snex  37283  finxpreclem4  37649  poimirlem16  37887  poimirlem17  37888  voliunnfl  37915  mbfresfi  37917  itg2addnclem2  37923  dvasin  37955  heiborlem4  38065  heiborlem6  38067  itrere  42688  sn-itrere  42858  sn-retire  42859  wepwsolem  43399  flcidc  43527  iocmbl  43570  arearect  43572  omcl3g  43691  iscard4  43889  briunov2uz  44054  eliunov2uz  44055  frege124d  44117  frege129d  44119  frege92  44311  lhe4.4ex1a  44685  dvconstbi  44690  binomcxplemnn0  44705  binomcxplemnotnn0  44712  infxr  45725  infleinflem2  45729  climneg  45970  cncfiooicc  46252  itgsinexplem1  46312  volioof  46345  stoweidlem36  46394  wallispilem3  46425  fourierdlem93  46557  fouriersw  46589  fouriercn  46590  etransclem16  46608  etransclem33  46625  sge0reuz  46805  nnfoctbdjlem  46813  hoidmvlelem3  46955  sinnpoly  47251  dfatafv2ex  47573  sprsymrelfvlem  47850  fmtnofz04prm  47937  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  gpg3nbgrvtx0  48436  lincext2  48815  blennn0elnn  48937  itcovalsucov  49028  resccat  49433  funcf2lem2  49441  isnatd  49582  swapfelvv  49622  fucoelvv  49679  prcofelvv  49739  termco  49840  prstcprs  49919