MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrdv Unicode version

Theorem ssrdv 3185
Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
Assertion
Ref Expression
ssrdv  |-  ( ph  ->  A  C_  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
21alrimiv 1617 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3169 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 203 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  sscon  3310  ssdif  3311  unss1  3344  ssrin  3394  eq0rdv  3489  uniss  3848  intss1  3877  intmin  3882  intssuni  3884  iunss1  3916  iinss1  3917  ss2iun  3920  ssiun  3944  ssiun2  3945  iinss  3953  iinss2  3954  trintss  4129  sspwb  4223  pwssun  4299  tron  4415  tz7.7  4418  ssorduni  4577  onint  4586  limsssuc  4641  limuni3  4643  limomss  4661  xpsspw  4797  relop  4834  dmss  4878  dmcosseq  4946  ssrnres  5116  sossfld  5120  dffv2  5592  chfnrn  5636  suppss  5658  dff3  5673  ffnfv  5685  f1imass  5788  fo1stres  6143  fo2ndres  6144  fnse  6232  reldmtpos  6242  onfununi  6358  smoiun  6378  smorndom  6385  tz7.48-1  6455  tz7.49  6457  oaass  6559  qsss  6720  pmss12g  6794  mapss  6810  ixpssmap2g  6845  ixpssmapg  6846  fineqv  7078  pssnn  7081  ssfii  7172  dffi2  7176  ordtypelem9  7241  ordtypelem10  7242  oismo  7255  unxpwdom2  7302  inf3lemd  7328  inf3lem1  7329  inf3lem6  7334  cantnflem3  7393  cantnf  7395  cnfcom3lem  7406  onssr1  7503  rankunb  7522  tcrank  7554  harcard  7611  carduni  7614  infxpenlem  7641  infpwfien  7689  dfac12r  7772  ackbij2lem1  7845  ackbij1lem18  7863  isfin1-3  8012  fin1a2lem11  8036  fin1a2lem13  8038  zorn2lem4  8126  zorn2lem5  8127  ttukeylem6  8141  ttukeylem7  8142  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2  8265  wunr1om  8341  wunom  8342  tskr1om  8389  tskr1om2  8390  tskxpss  8394  tskcard  8403  tskuni  8405  grothomex  8451  genpss  8628  distrlem1pr  8649  distrlem5pr  8651  prlem934  8657  ltexprlem2  8661  ltexprlem6  8665  ltexprlem7  8666  reclem3pr  8673  reclem4pr  8674  supmul1  9719  supmullem2  9721  peano5uzi  10100  uzss  10248  ixxdisj  10671  ixxss1  10674  ixxss2  10675  ixxss12  10676  ixxub  10677  ixxlb  10678  iocssre  10729  icossre  10730  iccssre  10731  icodisj  10761  fzss1  10830  fzss2  10831  fzosplit  10899  fzouzsplit  10901  sswrd  11423  isercoll  12141  summolem2a  12188  fsumcvg3  12202  fsum2dlem  12233  fsumcom2  12237  qshash  12285  bitsfzo  12626  phimullem  12847  prmreclem5  12967  1arith  12974  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  ramtlecl  13047  monhom  13638  epihom  13645  funcsetcres2  13925  psdmrn  14316  psssdm2  14324  gsumwspan  14468  frmdss2  14485  ssnmz  14659  conjnmz  14716  gex1  14902  sylow2alem1  14928  sylow3lem3  14940  lsmless1x  14955  lsmless2x  14956  lsmub1x  14957  lsmub2x  14958  lsmmod  14984  lsmdisj2  14991  efgrelexlemb  15059  efgcpbllemb  15064  cntzcmn  15136  gsum2d2  15225  dprdub  15260  dprdss  15264  dprddisj2  15274  ablfacrp  15301  pgpfac1lem3  15312  isdrng2  15522  subrguss  15560  subrgmre  15569  lssssr  15710  lsssssubg  15715  lssmre  15723  lbspss  15835  lspdisj  15878  lbsextlem2  15912  lidl1el  15970  drngnidl  15981  lpiss  16002  unitrrg  16034  fidomndrng  16048  mplbas2  16212  zsssubrg  16430  qsssubdrg  16431  cnsubrg  16432  mulgrhm2  16461  znrrg  16519  ocvocv  16571  ocv2ss  16573  ocvin  16574  lsmcss  16592  cssmre  16593  pjfo  16615  pjcss  16616  obs2ss  16629  bastg  16704  tgss  16706  tgtop  16711  tgidm  16718  en2top  16723  neisspw  16844  topssnei  16861  lpss3  16876  clslp  16879  tgrest  16890  ssrest  16907  restfpw  16910  restntr  16912  ordtbas2  16921  ordtbas  16922  cnss1  17005  cnss2  17006  cnsscnp  17008  cnrest2r  17015  cmpsublem  17126  cmpsub  17127  tgcmp  17128  cmpcld  17129  hauscmplem  17133  cnconn  17148  2ndcsep  17185  llyss  17205  nllyss  17206  restnlly  17208  restlly  17209  kgenss  17238  kgenidm  17242  llycmpkgen2  17245  1stckgen  17249  kgen2ss  17250  kgencn3  17253  ptbasfi  17276  ptpjopn  17306  ptclsg  17309  txdis  17326  txkgen  17346  xkoptsub  17348  xkopjcn  17350  txcon  17383  qtoptop2  17390  qtopuni  17393  qtopkgen  17401  basqtop  17402  tgqtop  17403  qtopss  17406  qtoprest  17408  qtopomap  17409  qtopcmap  17410  kqsat  17422  kqcldsat  17424  hmphdis  17487  isfild  17553  ssfg  17567  fgss  17568  fgss2  17569  fgfil  17570  fgabs  17574  filcon  17578  fgtr  17585  trfg  17586  uzrest  17592  ufilmax  17602  ufileu  17614  filufint  17615  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  flimss2  17667  flimss1  17668  flimclsi  17673  flimcf  17677  flimsncls  17681  fclssscls  17713  fclsss1  17717  fclsss2  17718  fclscf  17720  uffclsflim  17726  alexsublem  17738  alexsubALTlem3  17743  ptcmplem2  17747  ptcmplem3  17748  symgtgp  17784  cldsubg  17793  tsmscl  17817  haustsms2  17819  tgptsmscls  17832  tsmsxp  17837  xblss2  17958  unirnbl  17969  xrsblre  18317  xrsmopn  18318  recld2  18320  zdis  18322  icccmplem2  18328  cncfss  18403  cnheiborlem  18452  htpycn  18471  phtpyhtpy  18480  pi1blem  18537  clsocv  18677  cfilfcls  18700  iscmet3lem2  18718  iscmet2  18720  caussi  18723  equivcfil  18725  lmcau  18738  cmetss  18740  pjth  18803  hlhil  18807  ivthicc  18818  ovoliunnul  18866  ovolicopnf  18883  uniioombllem3  18940  dyadmbllem  18954  opnmbllem  18956  volsup2  18960  vitalilem2  18964  itg1addlem4  19054  itg10a  19065  itg1ge0a  19066  mbfi1fseqlem4  19073  itg2gt0  19115  limciun  19244  perfdvf  19253  dvidlem  19265  cpnord  19284  dvaddf  19291  dvmulf  19292  dvcof  19297  dvcj  19299  dvrec  19304  dvcnv  19324  dvlip2  19342  dvivth  19357  dvne0  19358  dvcnvre  19366  ftc1cn  19390  ply1lpir  19564  plyco0  19574  plyexmo  19693  ulmdv  19780  pserdv  19805  abelth  19817  efif1o  19908  logno1  19983  efopnlem2  20004  loglesqr  20098  ppisval  20341  ppisval2  20342  ppinprm  20390  chtnprm  20392  fsumvma  20452  dchrfi  20494  chtppilimlem2  20623  chebbnd2  20626  vmadivsumb  20632  rplogsumlem2  20634  dchrisumlem2  20639  vmalogdivsum2  20687  vmalogdivsum  20688  2vmadivsumlem  20689  selbergb  20698  selberg2b  20701  selberg3lem1  20706  selberg3lem2  20707  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  ococss  21872  shsub1  21903  shless  21938  shmodsi  21968  pjhth  21972  spansnss  22150  spanpr  22159  spansnm0i  22229  pjjsi  22279  sumdmdii  22995  sumdmdlem  22998  sumdmdlem2  22999  cdj3lem1  23014  abrexss  23040  ssnnssfz  23277  tpr2rico  23296  esumpcvgval  23446  cldssbrsiga  23518  measdivcstOLD  23551  measdivcst  23552  mbfmcnt  23573  sconpi1  23770  cvmscld  23804  cvmsss2  23805  cvmliftlem15  23829  rtrclreclem.trans  24043  dfon2lem6  24144  predpo  24184  preddowncl  24196  wfrlem10  24265  nofulllem5  24360  uninqs  25039  domintrefc  25125  iccss3  25134  npincppr  25159  nsn  25530  limfn  25565  islimrs3  25581  islimrs4  25582  icccon2  25700  icccon3  25701  icccon4  25702  rdmob  25748  rcmob  25749  tareltsuc  25898  fnctartar  25907  fnctartar2  25908  segline  26141  pxysxy  26142  fnessref  26293  locfincmp  26304  locfincf  26306  fgmin  26319  tailfb  26326  lpss2  26468  sstotbnd3  26500  prdstotbnd  26518  cntotbnd  26520  ismtyhmeo  26529  1idl  26651  eldiophss  26854  rencldnfilem  26903  pellexlem5  26918  pell14qrss1234  26941  pell1qrss14  26953  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  harinf  27127  kercvrlsm  27181  pwssplit4  27191  frlmsslsp  27248  lindfrn  27291  hbtlem5  27332  proot1hash  27519  refsumcn  27701  stoweidlem27  27776  stoweidlem46  27795  stoweidlem57  27806  ffnafv  28033  trsspwALT3  28594  bnj1033  28999  bnj1398  29064  lshpdisj  29177  lssats  29202  lkrlsp  29292  lkrin  29354  glbconxN  29567  paddss1  30006  paddss2  30007  paddasslem16  30024  paddidm  30030  pmodlem2  30036  pmapjoin  30041  pmapjat1  30042  pclfinN  30089  pclfinclN  30139  cdleme50rnlem  30733  diasslssN  31249  dia2dimlem12  31265  dihsslss  31466  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmaprnN  32057  hgmaprnN  32094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator