Theorem ssriv 3507

Description: Inference rule based on subclass definition. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
ssriv.1

Assertion

Ref	Expression
ssriv

Distinct variable groups:   ,   ,

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 3492	. 2
2		ssriv.1	. 2
3	1, 2	mpgbir 1622	1

Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475

This theorem is referenced by:  ssid  3522  ssv  3523  difss  3630  ssun1  3666  inss1  3717  0ss  3814  difprsnss  4165  snsspw  4201  uniin  4269  iuniin  4341  iunpwss  4420  pwuni  4683  pwunss  4790  xpsspw  5121  dmin  5215  dmrnssfld  5266  dmcoss  5267  dminss  5425  imainss  5426  fviss  5931  mapsspm  7472  pmsspw  7473  uniixp  7512  pwfilem  7834  dffi3  7911  dfom3  8085  onwf  8269  tcrank  8323  cardprclem  8381  alephsson  8502  ackbij1  8639  cardcf  8653  cfeq0  8657  dfacfin7  8800  hsmexlem6  8832  canthnum  9048  inaprc  9235  nqerf  9329  addnqf  9347  mulnqf  9348  dmrecnq  9367  reclem2pr  9447  wuncn  9568  zssre  10896  zsscn  10897  nnssz  10909  elq  11213  zssq  11218  qssre  11221  rpssre  11259  ixxssixx  11572  iooval2  11591  ioossre  11615  rge0ssre  11657  fzssuz  11753  fzssp1  11755  uzdisj  11780  nn0disj  11820  fzossfz  11846  fzouzsplit  11860  fzossnn  11870  fzo0ssnn0  11896  uzrdgfni  12069  seqcoll  12512  wrdexg  12557  wrdexb  12558  fclim  13376  isercolllem3  13489  isercoll  13490  climcnds  13663  divcnv  13665  harmonic  13670  mertenslem1  13693  bitsss  14076  maxprmfct  14254  prminf  14433  prmreclem2  14435  prmreclem3  14436  1arithlem1  14441  1arith  14445  4sqlem19  14481  vdwlem12  14510  restsspw  14829  xpsc0  14957  xpsc1  14958  mremre  15001  mreacs  15055  isfunc  15233  homarel  15363  ledm  15854  lern  15855  sgrpssmgm  16051  mndsssgrp  16052  prdsgrpd  16179  prdsinvgd  16180  symgtrf  16494  odf1o2  16593  sylow3lem3  16649  sylow3lem6  16652  oppglsm  16662  efgsfo  16757  0frgp  16797  prdscmnd  16867  prdsabld  16868  gsummptnn0fz  17014  dprdssv  17056  dprdres  17075  ablfac1b  17121  prdsringd  17261  prdscrngd  17262  unitss  17309  subrgint  17451  lssintcl  17610  prdslmodd  17615  psrbaglefi  18023  psrbaglefiOLD  18024  coe1mul2lem2  18309  xrge0subm  18459  cnsubmlem  18466  cnsubglem  18467  cnsubdrglem  18469  cnmsubglem  18480  zringlpir  18512  zlpir  18517  zringunit  18520  zrngunit  18521  znf1o  18590  zntoslem  18595  ocvss  18701  dsmmsubg  18774  dsmmlss  18775  lbslinds  18868  unitg  19468  cldss2  19531  indiscld  19592  toponmre  19594  iscldtop  19596  1stcfb  19946  llyssnlly  19979  llyidm  19989  nllyidm  19990  toplly  19991  hauslly  19993  lly1stc  19997  dissnref  20029  1stckgenlem  20054  txindis  20135  pthaus  20139  ptcmpfi  20314  ufinffr  20430  cnflf2  20504  flimfcls  20527  alexsubALTlem3  20549  ptcmplem1  20552  ptcmpg  20557  prdstmdd  20622  prdstgpd  20623  ust0  20722  prdsms  21034  qdensere  21277  blssioo  21300  tgioo  21301  xrtgioo  21311  xrsmopn  21317  zdis  21321  reperflem  21323  xrge0gsumle  21338  xrge0tsms  21339  icopnfhmeo  21443  bndth  21458  ovoliunlem1  21913  ovoliun2  21917  ovolicc2lem4  21931  voliunlem2  21961  voliunlem3  21962  uniioovol  21988  uniioombllem4  21995  vitali  22022  ismbf3d  22061  itg2seq  22149  limccl  22279  limcresi  22289  dvef  22381  plypf1  22609  aasscn  22714  qssaa  22720  aannenlem1  22724  aannenlem2  22725  aannenlem3  22726  ulmcn  22794  mtestbdd  22800  iblulm  22802  reeff1o  22842  reefgim  22845  efifo  22934  dfrelog  22953  relogf1o  22954  logdmss  23023  logcn  23028  dvloglem  23029  logf1o2  23031  dvlog  23032  dvlog2lem  23033  dvlog2  23034  logtayl  23041  cxpcn  23119  cxpcn2  23120  cxpcn3  23122  resqrtcn  23123  efrlim  23299  dfef2  23300  cxp2lim  23306  wilthlem2  23343  wilthlem3  23344  basellem3  23356  basellem4  23357  prmdvdsfi  23381  vmaval  23387  mumul  23455  sqff1o  23456  musum  23467  fsumvma2  23489  dchrmhm  23516  chtppilim  23660  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  dchrisumlema  23673  dchrmusum2  23679  dchrvmasum2lem  23681  dirith2  23713  mudivsum  23715  mulogsum  23717  mulog2sumlem2  23720  selberg2lem  23735  selberg3lem2  23743  pntrsumo1  23750  pnt2  23798  pnt  23799  axcontlem2  24268  usgraexmpl  24401  wwlksswrd  24688  wwlksswwlkn  24703  clwlksarewlks  24759  iseupa  24965  phrel  25730  bnrel  25783  hlrel  25806  shex  26129  chsssh  26143  hhssnv  26180  choc1  26245  shunssi  26286  shsleji  26288  shsub1i  26290  shsub2i  26291  shsidmi  26302  omlsii  26321  spanuni  26462  spansni  26475  5oalem7  26578  3oalem3  26582  pjrni  26620  mayete3i  26646  mayete3iOLD  26647  hmopex  26794  cnlnssadj  26999  adjbdln  27002  adjsslnop  27006  shatomistici  27280  hatomistici  27281  xrge0tsmsd  27775  esumpcvgval  28084  hashf2  28090  insiga  28137  sxbrsigalem0  28242  dya2icobrsiga  28247  sxbrsigalem1  28256  sxbrsigalem2  28257  eulerpartlemb  28307  lgamgulm2  28578  lgamcvglem  28582  erdszelem9  28643  erdsze2lem2  28648  kur14lem9  28658  ptpcon  28678  iinllycon  28699  cvmlift3  28773  mppsthm  28939  imagesset  29603  altxpsspw  29627  bpolylem  29810  onsstopbas  29894  onsucconi  29902  onintopsscon  29905  onint1  29914  oninhaus  29915  topjoin  30183  heiborlem3  30309  eldioph3b  30698  diophin  30706  diophun  30707  eldiophss  30708  fz1ssnn  30744  isnumbasabl  31055  isnumbasgrp  31056  dfacbasgrp  31057  mon1psubm  31166  nzin  31223  fzssz  31466  rrpsscn  31582  fprodge0  31597  dvnmul  31740  dvnprodlem2  31744  stoweidlem34  31816  stirlinglem13  31868  fourierdlem20  31909  fourierdlem62  31951  fourierdlem83  31972  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fouriersw  32014  ringssrng  32686  srhmsubc  32884  srhmsubcOLD  32903  lvecpsslmod  33108  aacllem  33216  unipwrVD  33632  unipwr  33633  bnj1398  34090  bnj1498  34117  bj-snglss  34528  bj-modssabl  34658  atssbase  35015  intimass  37768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489