MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eqel Structured version   Visualization version   GIF version

Theorem syl6eqel 2900
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqel.1 (𝜑𝐴 = 𝐵)
syl6eqel.2 𝐵𝐶
Assertion
Ref Expression
syl6eqel (𝜑𝐴𝐶)

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqel.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqeltrd 2892 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2806  df-clel 2809
This theorem is referenced by:  syl6eqelr  2901  csbexg  4994  unisn2  4996  class2set  5031  snexALT  5059  snex  5105  prex  5106  onun2i  6059  iotaex  6084  fvrn0  6439  f0cli  6595  funsneqopOLD  6645  funsneqopb  6646  fmptsng  6662  fmptsnd  6663  elimdelov  6969  ovima0  7046  ndmovcl  7052  caovmo  7104  soex  7342  zfrep6  7367  1st2ndb  7441  wfrlem17  7670  smofvon2  7692  tz7.44-2  7742  oesuclem  7845  omcl  7856  oecl  7857  nnmcl  7932  nnecl  7933  ixpexg  8172  resixpfo  8186  en1b  8263  xpsnen  8286  nnunifi  8453  xpfi  8473  fsuppun  8536  0fsupp  8539  oiexg  8682  hartogslem1  8689  cantnfvalf  8812  rankdmr1  8914  rankr1c  8934  numwdom  9168  alephon  9178  isfin5  9409  sdom2en01  9412  isf32lem9  9471  hsmexlem9  9535  iundom2g  9650  gchxpidm  9779  r1tskina  9892  tskmcl  9951  recmulnq  10074  recclnq  10076  genpelv  10110  un0mulcl  11596  znegcl  11681  zeo  11732  eqreznegel  11996  xnegcl  12265  xnn0xaddcl  12287  ioorebas  12497  modid0  12923  2txmodxeq0  12957  fzofi  13000  expcllem  13097  m1expcl2  13108  faclbnd4lem3  13305  bccl  13332  hasheq0  13375  hashrabrsn  13382  fnfz0hashnn0  13452  fnfzo0hashnn0  13455  ccat2s1p1  13630  cshwcl  13771  relexpaddg  14019  abs00bd  14257  iserge0  14617  sumrblem  14668  fsumcvg  14669  summolem2a  14672  sumss  14681  fsumss  14682  fsumcvg2  14684  sumsplit  14725  binom  14787  bcxmas  14792  geomulcvg  14832  prodrblem  14883  fprodcvg  14884  prodmolem2a  14888  zprod  14891  fprodntriv  14896  prodss  14901  fprodss  14902  binomfallfac  14995  bpoly1  15005  bpoly2  15011  bpoly3  15012  ruclem6  15187  smupf  15422  gcdcl  15450  lcmcl  15536  lcmfcl  15563  pcxcl  15785  pcmptcl  15815  infpnlem2  15835  zgz  15857  4sqlem2  15873  4sqlem19  15887  vdwapval  15897  hashbc0  15929  ramcl2  15940  0ramcl  15947  ramcl  15953  isstruct2  16081  imasval  16379  imasbas  16380  imasds  16381  imasplusg  16385  imasmulr  16386  imasvsca  16388  imasip  16389  imasle  16391  qusaddvallem  16419  qusaddflem  16420  qusaddval  16421  qusaddf  16422  qusmulval  16423  qusmulf  16424  mreexexlem3d  16514  sscpwex  16682  fullresc  16718  estrresOLD  16986  estrres  16987  evlfcl  17070  ipopos  17368  gsumress  17484  submnd0  17528  qusgrp2  17741  issubg2  17814  torsubg  18461  frgpnabllem1  18480  lt6abl  18500  ablfaclem3  18691  ablfac2  18693  srgbinomlem3  18747  ringidss  18782  qusring2  18825  isdrngd  18979  mptscmfsupp0  19135  islss3  19169  lspsnel  19213  lspprel  19304  znf1o  20110  frgpcyg  20132  cnmsgnsubg  20133  phlpropd  20213  cssval  20240  iscss  20241  dsmm0cl  20298  uvcvvcl  20340  m1detdiag  20618  m2detleiblem1  20645  pmatcollpw3fi1lem1  20808  indistopon  21023  indiscld  21113  restbas  21180  ordttopon  21215  iocpnfordt  21237  icomnfordt  21238  lecldbas  21241  fiuncmp  21425  cmpfi  21429  conncompid  21452  dissnlocfin  21550  elpt  21593  xkotop  21609  xkouni  21620  xkohaus  21674  xkoptsub  21675  imastopn  21741  filconn  21904  cfinufil  21949  alexsublem  22065  alexsub  22066  alexsubALTlem4  22071  distgp  22120  indistgp  22121  ssblps  22444  ssbl  22445  xmeter  22455  nmoi  22749  nmoeq0  22757  0nghm  22762  idnghm  22764  icccld  22787  iocmnfcld  22789  blssioo  22815  xrtgioo  22826  xrsxmet  22829  icccmp  22845  pcopt  23038  pcopt2  23039  elpi1  23061  cmetcaulem  23303  ishl2  23383  rrxmvallem  23405  ovolcl  23465  ovolunlem1a  23483  ovolunnul  23487  ovoliunnul  23494  ioombl1  23549  icombl  23551  ioombl  23552  iccmbl  23553  iccvolcl  23554  ovolioo  23555  ioovolcl  23557  ioorcl  23564  uniioovol  23566  uniioombllem2a  23569  uniioombllem4  23573  uniioombllem5  23574  vitalilem1  23595  vitalilem5  23599  mbfconstlem  23614  mbfima  23617  mbfid  23622  ismbf2d  23627  mbfss  23633  mbfmulc2lem  23634  i1fd  23668  itg1addlem2  23684  itg1addlem4  23686  itg1addlem5  23687  i1fmulc  23690  itg2l  23716  itg2cl  23719  ibl0  23773  iblrelem  23777  iblpos  23779  iblss2  23792  bddmulibl  23825  recnperf  23889  ply1remlem  24142  fta1glem1  24145  fta1g  24147  elply  24171  plypf1  24188  coefv0  24224  coemulc  24231  fta1  24283  elqaalem2  24295  aannenlem2  24304  aalioulem3  24309  taylfvallem1  24331  tayl0  24336  ulm0  24365  logtayl  24626  atanrecl  24858  atanbnd  24873  harmonicbnd3  24954  ftalem7  25025  basellem5  25031  ppifi  25052  sqff1o  25128  1sgmprm  25144  logexprlim  25170  dchrelbasd  25184  dchr1re  25208  lgslem4  25245  lgsne0  25280  2sqlem9  25372  2sqlem10  25373  rpvmasumlem  25396  dchrisumlem1  25398  vmalogdivsum  25448  pntrlog2bndlem5  25490  ostth  25548  tgcgr4  25646  axlowdimlem16  26057  fusgrfisbase  26442  vtxdg0e  26604  rgrusgrprc  26719  clwwlknfi  27200  trlsegvdeglem7  27405  eulerpathpr  27419  0blo  27981  nmlno0lem  27982  omlsilem  28595  pjoc1i  28624  nonbooli  28844  nmlnop0iALT  29188  unopbd  29208  leoprf2  29320  opsqrlem4  29336  opsqrlem5  29337  pjbdlni  29342  pjcmul1i  29394  prsssdm  30294  ordtrestNEW  30298  esumpad  30448  esumpad2  30449  esumcst  30456  esumrnmpt2  30461  sibf0  30727  sitgclcn  30737  sitgclre  30738  eulerpartlemgs2  30773  dstfrvclim1  30870  ballotlemfelz  30883  sgncl  30931  signstfveq0  30985  breprexp  31042  subfacp1lem3  31492  rellysconn  31561  cvmlift2lem9  31621  ordcmp  32768  finxpreclem4  33549  poimirlem16  33740  poimirlem17  33741  voliunnfl  33768  mbfresfi  33770  itg2addnclem2  33776  bddiblnc  33794  dvasin  33810  heiborlem4  33926  heiborlem6  33928  wepwsolem  38114  flcidc  38246  iocmbl  38299  arearect  38302  briunov2uz  38491  eliunov2uz  38492  frege124d  38554  frege129d  38556  frege92  38750  lhe4.4ex1a  39029  dvconstbi  39034  binomcxplemnn0  39049  binomcxplemnotnn0  39056  infxr  40064  infleinflem2  40068  climneg  40323  cncfiooicc  40588  itgsinexplem1  40650  volioof  40684  stoweidlem36  40733  wallispilem3  40764  fourierdlem93  40896  fouriersw  40928  fouriercn  40929  etransclem16  40947  etransclem33  40964  sge0reuz  41144  nnfoctbdjlem  41152  hoidmvlelem3  41294  dfatafv2ex  41803  fmtnofz04prm  42065  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  sprsymrelfvlem  42309  lincext2  42813  blennn0elnn  42940
  Copyright terms: Public domain W3C validator