Theorem syl6eleqr 2712

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
syl6eleqr.1	|- ( ph -> A e. B )
syl6eleqr.2	|- C = B

Assertion

Ref	Expression
syl6eleqr	|- ( ph -> A e. C )

Proof of Theorem syl6eleqr

Step	Hyp	Ref	Expression
1		syl6eleqr.1	. 2 |- ( ph -> A e. B )
2		syl6eleqr.2	. . 3 |- C = B
3	2	eqcomi 2631	. 2 |- B = C
4	1, 3	syl6eleq 2711	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  3eltr4g  2718  tpnzd  4314  brelrng  5355  elabrex  6501  fliftel1  6560  ovidig  6778  unielxp  7204  tfrlem11  7484  rdglim  7522  seqomlem4  7548  2oconcl  7583  ecopqsi  7804  erov  7844  eroprf  7845  sbthlem2  8071  dffi3  8337  ixpiunwdom  8496  cantnfcl  8564  r1lim  8635  rankwflemb  8656  pwwf  8670  unwf  8673  rankwflem  8678  uniwf  8682  rankpwi  8686  rankr1g  8695  r1pw  8708  r1rankid  8722  rankuni  8726  cardlim  8798  infxpenlem  8836  alephfp  8931  cfsmolem  9092  alephsing  9098  hsmexlem4  9251  axdc3lem2  9273  numth3  9292  iunfo  9361  konigthlem  9390  iunctb  9396  canthwelem  9472  canthwe  9473  r1limwun  9558  inar1  9597  inatsk  9600  gruina  9640  grur1  9642  tskmval  9661  tskmcl  9663  pinq  9749  dmrecnq  9790  addclsr  9904  mulclsr  9905  axaddf  9966  axmulf  9967  peano2nn  11032  uztrn2  11705  eluz2nn  11726  peano2uzs  11742  uzsupss  11780  uzsup  12662  uzrdgfni  12757  uzrdgsuci  12759  fsuppmapnn0fiub  12790  seqf  12822  ser0  12853  bcm1k  13102  bcp1nk  13104  bcpasc  13108  hashprdifel  13186  fz1isolem  13245  pr2pwpr  13261  ccatrn  13372  ccats1val2  13404  swrdccatin12lem3  13490  rexuzre  14092  limsupgre  14212  climconst  14274  rlimclim1  14276  climrlim2  14278  clim2ser  14385  clim2ser2  14386  iserex  14387  isermulc2  14388  iserle  14390  isercolllem3  14397  isercoll2  14399  climsup  14400  iseraltlem2  14413  iseraltlem3  14414  zsum  14449  isumclim3  14490  isumadd  14498  fsump1i  14500  iserabs  14547  cvgcmp  14548  cvgcmpub  14549  cvgcmpce  14550  abscvgcvg  14551  isumshft  14571  isumsplit  14572  isum1p  14573  isumrpcl  14575  isumsup2  14578  climcndslem1  14581  cvgrat  14615  clim2prod  14620  clim2div  14621  prodf1  14623  ntrivcvgn0  14630  ntrivcvgtail  14632  fprodntriv  14672  fprodabs  14704  fprodeq0  14705  iprodclim3  14731  iprodmul  14734  ef0lem  14809  fprodefsum  14825  rpnnen2lem3  14945  dvdsflip  15039  fzo0dvdseq  15045  bitsinv1  15164  smupval  15210  smueqlem  15212  seq1st  15284  algr0  15285  prmind2  15398  crth  15483  eulerthlem2  15487  prmdiv  15490  pockthlem  15609  pockthg  15610  unbenlem  15612  prmunb  15618  prmgaplem7  15761  strfv2d  15905  imasvscaval  16198  oppccatid  16379  epii  16403  fthepi  16588  funcestrcsetclem3  16782  funcsetcestrclem3  16796  yon12  16905  yon2  16906  yonedalem4c  16917  yonedalem22  16918  yonedalem3b  16919  yonedainv  16921  acsmapd  17178  mgm2nsgrplem1  17405  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem1  17410  sgrp2rid2  17413  cntrsubgnsg  17773  pmtrrn  17877  gexcl3  18002  efgi  18132  efgi2  18138  efgs1b  18149  efgredlemg  18155  efgredlemd  18157  frgpnabllem1  18276  cycsubgcyg  18302  gsumzaddlem  18321  dprdwd  18410  dprd2da  18441  lsppratlem3  19149  lsppratlem4  19150  lbsextlem2  19159  lidl0  19219  lidl1  19220  mplsubrglem  19439  mpfconst  19530  mpfproj  19531  mpfind  19536  pf1const  19710  pf1id  19711  mpfpf1  19715  pf1mpf  19716  domnchr  19880  znf1o  19900  madetsumid  20267  slesolex  20488  pmatcoe1fsupp  20506  mat2pmatbas0  20532  pmatcollpw  20586  pm2mpf1  20604  isclo  20891  indiscld  20895  restntr  20986  ordtbaslem  20992  ordtbas2  20995  lmconst  21065  lmss  21102  conncompid  21234  2ndcomap  21261  locfincmp  21329  comppfsc  21335  xkouni  21402  txcls  21407  ptclsg  21418  uptx  21428  txindis  21437  tx1stc  21453  cnmpt1res  21479  tgqtop  21515  uffix  21725  cnpflf2  21804  ptcmplem2  21857  ptcmplem4  21859  tgpconncomp  21916  tsmsfbas  21931  fmucnd  22096  prdsxmetlem  22173  imasdsf1olem  22178  prdsbl  22296  blcvx  22601  xrsmopn  22615  xrge0tsms  22637  metdcn2  22642  expcncf  22725  cnmpt2pc  22727  icchmeo  22740  iccpnfhmeo  22744  cnheibor  22754  evth  22758  evth2  22759  lebnumlem2  22761  lebnumii  22765  reparphti  22797  cfilfcls  23072  minveclem2  23197  minveclem3  23200  minveclem4  23203  ovoliunlem1  23270  ovolicc1  23284  iundisj  23316  volsup  23324  uniioombllem3  23353  vitalilem2  23378  vitalilem3  23379  mbfsup  23431  mbfinf  23432  mbflimsup  23433  itg2monolem1  23517  limcflflem  23644  limccnp  23655  limccnp2  23656  dvidlem  23679  dvn2bss  23693  cpnres  23700  dvcobr  23709  dvrec  23718  c1liplem1  23759  dvcnvrelem2  23781  dvfsumrlimf  23788  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlim  23794  dvfsum2  23797  coeeulem  23980  coeid3  23996  plycn  24017  dvntaylp  24125  taylthlem1  24127  taylthlem2  24128  ulm2  24139  ulmshftlem  24143  ulmshft  24144  ulm0  24145  ulmcn  24153  ulmdvlem3  24156  ulmdv  24157  mtest  24158  mtestbdd  24159  dvradcnv  24175  psercn2  24177  psercn  24180  pserdv  24183  abelth  24195  efif1olem2  24289  efif1olem4  24291  efifo  24293  eff1olem  24294  logcn  24393  dvloglem  24394  cxpcn3  24489  resqrtcn  24490  sqrtcn  24491  logbleb  24521  logblt  24522  asinneg  24613  atanlogsub  24643  atanbnd  24653  ressatans  24661  leibpilem2  24668  xrlimcnp  24695  efrlim  24696  scvxcvx  24712  ppiub  24929  chtub  24937  logexprlim  24950  lgseisenlem1  25100  rplogsumlem1  25173  rplogsumlem2  25174  dchrisumlem2  25179  dchrisum0flb  25199  logdivbnd  25245  pntlem3  25298  tgcgr4  25426  ltgov  25492  f1otrg  25751  eengtrkg  25865  iedgedg  25943  ushgredgedgloop  26123  subgruhgredgd  26176  nbgrel  26238  uvtxupgrres  26309  cplgr3v  26331  umgr2v2evd2  26423  edginwlk  26530  wlk1walk  26535  wlkres  26567  crctcshwlkn0lem6  26707  wlkiswwlks1  26753  wlknwwlksnfun  26774  wwlks2onv  26847  minvecolem1  27730  minvecolem2  27731  minvecolem4  27736  htthlem  27774  5oalem2  28514  3oalem2  28522  iundisjf  29402  fmptco1f1o  29434  xppreima  29449  xppreima2  29450  dfcnv2  29476  xrge0tsmsd  29785  rhmopp  29819  pmtrto1cl  29849  psgnfzto1stlem  29850  fzto1stfv1  29851  fzto1st  29853  fzto1stinvn  29854  psgnfzto1st  29855  smatlem  29863  smatcl  29868  tpr2rico  29958  xrmulc1cn  29976  xrge0mulc1cn  29987  esumpfinvallem  30136  ldgenpisyslem1  30226  dynkin  30230  brfae  30311  sxbrsigalem3  30334  dya2icoseg2  30340  omsmeas  30385  sibfof  30402  sseqmw  30453  sseqf  30454  sseqp1  30457  fiblem  30460  fibp1  30463  probfinmeasbOLD  30490  repr0  30689  reprpmtf1o  30704  hgt750lemg  30732  bnj1379  30901  subfacp1lem5  31166  subfacp1lem6  31167  cvxpconn  31224  cvxsconn  31225  cvmliftlem6  31272  cvmliftlem8  31274  cvmliftlem10  31276  cvmlift2lem6  31290  cvmlift2lem11  31295  cvmlift2lem12  31296  msubff  31427  msubco  31428  elmsta  31445  msubff1  31453  mvhf  31455  msubvrs  31457  iprodefisumlem  31626  filnetlem3  32375  knoppcnlem10  32492  knoppcnlem11  32493  icoreunrn  33207  icoreelrn  33209  poimirlem3  33412  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem30  33439  dvasin  33496  cover2  33508  upixp  33524  sdclem1  33539  fdc  33541  caushft  33557  ismtyres  33607  rrncmslem  33631  isfld2  33804  osumcllem10N  35251  pexmidlem7N  35262  dihglblem2N  36583  lcfrvalsnN  36830  lcfrlem5  36835  lcfrlem6  36836  lcfrlem27  36858  lcfrlem37  36868  monotuz  37506  expdiophlem1  37588  kelac2  37635  dvgrat  38511  nzss  38516  uzmptshftfval  38545  binomcxplemnotnn0  38555  refsumcn  39189  rfcnpre2  39190  rfcnpre3  39192  rfcnpre4  39193  elabrexg  39206  disjf1o  39378  unirnmap  39400  unirnmapsn  39406  ssmapsn  39408  mptssid  39450  allbutfi  39616  eluzd  39635  uzidd2  39643  ressiocsup  39781  ressioosup  39782  ressiooinf  39784  fsumsermpt  39811  climexp  39837  climinf  39838  climsuse  39840  sumnnodd  39862  limsupresico  39932  limsupubuzlem  39944  limsupresxr  39998  liminfresxr  39999  liminfresico  40003  limsup10exlem  40004  cnrefiisplem  40055  cncfiooicclem1  40106  dvsinax  40127  itgsinexplem1  40169  fvvolioof  40206  fvvolicof  40208  stoweidlem14  40231  stoweidlem16  40233  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem43  40260  stoweidlem46  40263  stoweidlem47  40264  stoweidlem52  40269  stoweidlem55  40272  stoweidlem57  40274  dirkercncf  40324  fourierdlem20  40344  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem54  40377  fourierdlem62  40385  fourierdlem71  40394  fourierdlem80  40403  fourierdlem114  40437  fouriersw  40448  ioorrnopnlem  40524  ioorrnopnxrlem  40526  salexct3  40560  salgencntex  40561  salgensscntex  40562  subsalsal  40577  sge0fodjrnlem  40633  sge0isum  40644  sge0seq  40663  sge0reuz  40664  sge0reuzb  40665  meadjiunlem  40682  meaiininclem  40700  carageniuncllem1  40735  caratheodorylem1  40740  hoiprodp1  40802  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  voncmpl  40835  hoiqssbl  40839  smflimlem2  40980  smfsuplem1  41017  smfsuplem3  41019  afvres  41252  iccpartigtl  41359  sprsymrelf  41745  funcringcsetcALTV2lem3  42038  funcringcsetclem3ALTV  42061  lindslinindsimp2lem5  42251  onsetreclem3  42450  amgmwlem  42548