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

Theorem ssrdv 3187
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 1619 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3171 . 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 1529    e. wcel 1686    C_ wss 3154
This theorem is referenced by:  sscon  3312  ssdif  3313  unss1  3346  ssrin  3396  eq0rdv  3491  uniss  3850  intss1  3879  intmin  3884  intssuni  3886  iunss1  3918  iinss1  3919  ss2iun  3922  ssiun  3946  ssiun2  3947  iinss  3955  iinss2  3956  trintss  4131  sspwb  4225  pwssun  4301  tron  4417  tz7.7  4420  ssorduni  4579  onint  4588  limsssuc  4643  limuni3  4645  limomss  4663  xpsspw  4799  relop  4836  dmss  4880  dmcosseq  4948  ssrnres  5118  sossfld  5122  dffv2  5594  chfnrn  5638  suppss  5660  dff3  5675  ffnfv  5687  f1imass  5790  fo1stres  6145  fo2ndres  6146  fnse  6234  reldmtpos  6244  onfununi  6360  smoiun  6380  smorndom  6387  tz7.48-1  6457  tz7.49  6459  oaass  6561  qsss  6722  pmss12g  6796  mapss  6812  ixpssmap2g  6847  ixpssmapg  6848  fineqv  7080  pssnn  7083  ssfii  7174  dffi2  7178  ordtypelem9  7243  ordtypelem10  7244  oismo  7257  unxpwdom2  7304  inf3lemd  7330  inf3lem1  7331  inf3lem6  7336  cantnflem3  7395  cantnf  7397  cnfcom3lem  7408  onssr1  7505  rankunb  7524  tcrank  7556  harcard  7613  carduni  7616  infxpenlem  7643  infpwfien  7691  dfac12r  7774  ackbij2lem1  7847  ackbij1lem18  7865  isfin1-3  8014  fin1a2lem11  8038  fin1a2lem13  8040  zorn2lem4  8128  zorn2lem5  8129  ttukeylem6  8143  ttukeylem7  8144  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2  8267  wunr1om  8343  wunom  8344  tskr1om  8391  tskr1om2  8392  tskxpss  8396  tskcard  8405  tskuni  8407  grothomex  8453  genpss  8630  distrlem1pr  8651  distrlem5pr  8653  prlem934  8659  ltexprlem2  8663  ltexprlem6  8667  ltexprlem7  8668  reclem3pr  8675  reclem4pr  8676  supmul1  9721  supmullem2  9723  peano5uzi  10102  uzss  10250  ixxdisj  10673  ixxss1  10676  ixxss2  10677  ixxss12  10678  ixxub  10679  ixxlb  10680  iocssre  10731  icossre  10732  iccssre  10733  icodisj  10763  fzss1  10832  fzss2  10833  fzosplit  10901  fzouzsplit  10903  sswrd  11425  isercoll  12143  summolem2a  12190  fsumcvg3  12204  fsum2dlem  12235  fsumcom2  12239  qshash  12287  bitsfzo  12628  phimullem  12849  prmreclem5  12969  1arith  12976  vdwlem2  13031  vdwlem6  13035  vdwlem8  13037  ramtlecl  13049  monhom  13640  epihom  13647  funcsetcres2  13927  psdmrn  14318  psssdm2  14326  gsumwspan  14470  frmdss2  14487  ssnmz  14661  conjnmz  14718  gex1  14904  sylow2alem1  14930  sylow3lem3  14942  lsmless1x  14957  lsmless2x  14958  lsmub1x  14959  lsmub2x  14960  lsmmod  14986  lsmdisj2  14993  efgrelexlemb  15061  efgcpbllemb  15066  cntzcmn  15138  gsum2d2  15227  dprdub  15262  dprdss  15266  dprddisj2  15276  ablfacrp  15303  pgpfac1lem3  15314  isdrng2  15524  subrguss  15562  subrgmre  15571  lssssr  15712  lsssssubg  15717  lssmre  15725  lbspss  15837  lspdisj  15880  lbsextlem2  15914  lidl1el  15972  drngnidl  15983  lpiss  16004  unitrrg  16036  fidomndrng  16050  mplbas2  16214  zsssubrg  16432  qsssubdrg  16433  cnsubrg  16434  mulgrhm2  16463  znrrg  16521  ocvocv  16573  ocv2ss  16575  ocvin  16576  lsmcss  16594  cssmre  16595  pjfo  16617  pjcss  16618  obs2ss  16631  bastg  16706  tgss  16708  tgtop  16713  tgidm  16720  en2top  16725  neisspw  16846  topssnei  16863  lpss3  16878  clslp  16881  tgrest  16892  ssrest  16909  restfpw  16912  restntr  16914  ordtbas2  16923  ordtbas  16924  cnss1  17007  cnss2  17008  cnsscnp  17010  cnrest2r  17017  cmpsublem  17128  cmpsub  17129  tgcmp  17130  cmpcld  17131  hauscmplem  17135  cnconn  17150  2ndcsep  17187  llyss  17207  nllyss  17208  restnlly  17210  restlly  17211  kgenss  17240  kgenidm  17244  llycmpkgen2  17247  1stckgen  17251  kgen2ss  17252  kgencn3  17255  ptbasfi  17278  ptpjopn  17308  ptclsg  17311  txdis  17328  txkgen  17348  xkoptsub  17350  xkopjcn  17352  txcon  17385  qtoptop2  17392  qtopuni  17395  qtopkgen  17403  basqtop  17404  tgqtop  17405  qtopss  17408  qtoprest  17410  qtopomap  17411  qtopcmap  17412  kqsat  17424  kqcldsat  17426  hmphdis  17489  isfild  17555  ssfg  17569  fgss  17570  fgss2  17571  fgfil  17572  fgabs  17576  filcon  17580  fgtr  17587  trfg  17588  uzrest  17594  ufilmax  17604  ufileu  17616  filufint  17617  rnelfm  17650  fmfnfmlem2  17652  fmfnfmlem4  17654  flimss2  17669  flimss1  17670  flimclsi  17675  flimcf  17679  flimsncls  17683  fclssscls  17715  fclsss1  17719  fclsss2  17720  fclscf  17722  uffclsflim  17728  alexsublem  17740  alexsubALTlem3  17745  ptcmplem2  17749  ptcmplem3  17750  symgtgp  17786  cldsubg  17795  tsmscl  17819  haustsms2  17821  tgptsmscls  17834  tsmsxp  17839  xblss2  17960  unirnbl  17971  xrsblre  18319  xrsmopn  18320  recld2  18322  zdis  18324  icccmplem2  18330  cncfss  18405  cnheiborlem  18454  htpycn  18473  phtpyhtpy  18482  pi1blem  18539  clsocv  18679  cfilfcls  18702  iscmet3lem2  18720  iscmet2  18722  caussi  18725  equivcfil  18727  lmcau  18740  cmetss  18742  pjth  18805  hlhil  18809  ivthicc  18820  ovoliunnul  18868  ovolicopnf  18885  uniioombllem3  18942  dyadmbllem  18956  opnmbllem  18958  volsup2  18962  vitalilem2  18966  itg1addlem4  19056  itg10a  19067  itg1ge0a  19068  mbfi1fseqlem4  19075  itg2gt0  19117  limciun  19246  perfdvf  19255  dvidlem  19267  cpnord  19286  dvaddf  19293  dvmulf  19294  dvcof  19299  dvcj  19301  dvrec  19306  dvcnv  19326  dvlip2  19344  dvivth  19359  dvne0  19360  dvcnvre  19368  ftc1cn  19392  ply1lpir  19566  plyco0  19576  plyexmo  19695  ulmdv  19782  pserdv  19807  abelth  19819  efif1o  19910  logno1  19985  efopnlem2  20006  loglesqr  20100  ppisval  20343  ppisval2  20344  ppinprm  20392  chtnprm  20394  fsumvma  20454  dchrfi  20496  chtppilimlem2  20625  chebbnd2  20628  vmadivsumb  20634  rplogsumlem2  20636  dchrisumlem2  20641  vmalogdivsum2  20689  vmalogdivsum  20690  2vmadivsumlem  20691  selbergb  20700  selberg2b  20703  selberg3lem1  20708  selberg3lem2  20709  selberg3  20710  selberg4lem1  20711  selberg4  20712  pntrlog2bndlem2  20729  pntrlog2bndlem4  20731  ococss  21874  shsub1  21905  shless  21940  shmodsi  21970  pjhth  21974  spansnss  22152  spanpr  22161  spansnm0i  22231  pjjsi  22281  sumdmdii  22997  sumdmdlem  23000  sumdmdlem2  23001  cdj3lem1  23016  abrexss  23042  ssnnssfz  23279  tpr2rico  23298  esumpcvgval  23448  cldssbrsiga  23520  measdivcstOLD  23553  measdivcst  23554  mbfmcnt  23575  sconpi1  23772  cvmscld  23806  cvmsss2  23807  cvmliftlem15  23831  rtrclreclem.trans  24045  dfon2lem6  24146  predpo  24186  preddowncl  24198  wfrlem10  24267  nofulllem5  24362  supaddc  24927  supadd  24928  uninqs  25050  domintrefc  25136  iccss3  25145  npincppr  25170  nsn  25541  limfn  25576  islimrs3  25592  islimrs4  25593  icccon2  25711  icccon3  25712  icccon4  25713  rdmob  25759  rcmob  25760  tareltsuc  25909  fnctartar  25918  fnctartar2  25919  segline  26152  pxysxy  26153  fnessref  26304  locfincmp  26315  locfincf  26317  fgmin  26330  tailfb  26337  lpss2  26479  sstotbnd3  26511  prdstotbnd  26529  cntotbnd  26531  ismtyhmeo  26540  1idl  26662  eldiophss  26865  rencldnfilem  26914  pellexlem5  26929  pell14qrss1234  26952  pell1qrss14  26964  pellfundre  26977  pellfundge  26978  pellfundlb  26980  pellfundglb  26981  harinf  27138  kercvrlsm  27192  pwssplit4  27202  frlmsslsp  27259  lindfrn  27302  hbtlem5  27343  proot1hash  27530  refsumcn  27712  stoweidlem27  27787  stoweidlem46  27806  stoweidlem57  27817  ffnafv  28044  trsspwALT3  28667  bnj1033  29072  bnj1398  29137  lshpdisj  29250  lssats  29275  lkrlsp  29365  lkrin  29427  glbconxN  29640  paddss1  30079  paddss2  30080  paddasslem16  30097  paddidm  30103  pmodlem2  30109  pmapjoin  30114  pmapjat1  30115  pclfinN  30162  pclfinclN  30212  cdleme50rnlem  30806  diasslssN  31322  dia2dimlem12  31338  dihsslss  31539  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmaprnN  32130  hgmaprnN  32167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator