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

Theorem ssriv 3970
Description: Inference 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
StepHypRef Expression
1 dfss2 3954 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1791 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  ssid  3988  ssv  3990  difss  4107  ssun1  4147  inss1  4204  0ss  4349  difprsnss  4726  snsspw  4769  uniin  4852  pwuni  4868  iuniin  4923  iunpwss  5021  pwunssOLD  5448  relopabi  5688  dmin  5774  dmrnssfld  5835  dmcoss  5836  dminss  6004  imainss  6005  fviss  6735  mapsspm  8430  pmsspw  8431  uniixp  8474  pwfilem  8807  dffi3  8884  dfom3  9099  onwf  9248  tcrank  9302  djuss  9338  djuunxp  9339  djuun  9344  cardprclem  9397  alephsson  9515  ackbij1  9649  cardcf  9663  cfeq0  9667  dfacfin7  9810  hsmexlem6  9842  canthnum  10060  inaprc  10247  nqerf  10341  addnqf  10359  mulnqf  10360  dmrecnq  10379  reclem2pr  10459  wuncn  10581  zssre  11977  zsscn  11978  nnssz  11991  elq  12339  zssq  12345  qssre  12348  ixxssixx  12742  iooval2  12761  ioossre  12788  rge0ssre  12834  fzssz  12899  fz1ssnn  12928  fzssuz  12938  fzssp1  12940  uzdisj  12970  fz0ssnn0  12992  nn0disj  13013  fzossfz  13046  fzouzsplit  13062  fzo0ssnn0  13108  uzrdgfni  13316  seqcoll  13812  wrdexgOLD  13862  wrdexb  13863  fclim  14900  isercolllem3  15013  climcnds  15196  divcnv  15198  harmonic  15204  bitsss  15765  prmssnn  16010  maxprmfct  16043  1arith  16253  4sqlem19  16289  vdwlem12  16318  restsspw  16695  mremre  16865  mreacs  16919  isfunc  17124  homarel  17286  ledm  17824  lern  17825  sgrpssmgm  18038  mndsssgrp  18039  prdsgrpd  18149  prdsinvgd  18150  symgtrf  18528  odf1o2  18629  sylow3lem3  18685  sylow3lem6  18688  oppglsm  18698  efgsfo  18796  0frgp  18836  prdscmnd  18912  prdsabld  18913  dprdssv  19069  dprdres  19081  prdsringd  19293  prdscrngd  19294  unitss  19341  subrgint  19488  subdrgint  19513  sdrgint  19514  primefld  19515  lssintcl  19667  prdslmodd  19672  xrge0subm  20516  cnsubmlem  20523  cnsubglem  20524  cnsubdrglem  20526  cnmsubglem  20538  zringunit  20565  zringlpir  20566  znf1o  20628  zntoslem  20633  ocvss  20744  dsmmsubg  20817  dsmmlss  20818  lbslinds  20907  unitg  21505  cldss2  21568  indiscld  21629  iscldtop  21633  llyssnlly  22016  llyidm  22026  nllyidm  22027  toplly  22028  hauslly  22030  lly1stc  22034  dissnref  22066  txindis  22172  pthaus  22176  ptcmpfi  22351  ufinffr  22467  cnflf2  22541  flimfcls  22564  alexsubALTlem3  22587  ptcmplem1  22590  ptcmpg  22595  prdstmdd  22661  prdstgpd  22662  ust0  22757  prdsms  23070  qdensere  23307  blssioo  23332  tgioo  23333  xrtgioo  23343  xrsmopn  23349  zdis  23353  reperflem  23355  xrge0gsumle  23370  xrge0tsms  23371  icopnfhmeo  23476  bndth  23491  voliunlem2  24081  voliunlem3  24082  vitali  24143  ismbf3d  24184  itg2seq  24272  limccl  24402  limcresi  24412  dvef  24506  aasscn  24836  qssaa  24842  aannenlem2  24847  aannenlem3  24848  ulmcn  24916  mtestbdd  24922  iblulm  24924  reeff1o  24964  reefgim  24967  efifo  25058  dfrelog  25076  relogf1o  25077  logdmss  25152  logcn  25157  dvloglem  25158  logf1o2  25160  dvlog  25161  dvlog2lem  25162  dvlog2  25163  logtayl  25170  cxpcn  25253  cxpcn2  25254  cxpcn3  25256  resqrtcn  25257  efrlim  25475  dfef2  25476  cxp2lim  25482  basellem3  25588  basellem4  25589  sqff1o  25687  dchrmhm  25745  chtppilim  25979  chto1lb  25982  chpchtlim  25983  chpo1ub  25984  dchrisumlema  25992  selberg2lem  26054  selberg3lem2  26062  pntrsumo1  26069  pnt2  26117  pnt  26118  axcontlem2  26679  usgrexmplef  26969  griedg0ssusgr  26975  nbgrssvtx  27052  nbgrssovtx  27071  uvtxssvtx  27100  rgrusgrprc  27299  clwlkswks  27485  wwlkssswrd  27568  wwlkssswwlksn  27572  wspthsswwlkn  27625  wspthsswwlknon  27628  clwwlksclwwlkn  27737  phrel  28520  bnrel  28572  hlrel  28595  shex  28917  chsssh  28930  hhssnv  28969  choc1  29032  shunssi  29073  shsleji  29075  shsub1i  29077  shsub2i  29078  shsidmi  29089  omlsii  29108  spanuni  29249  spansni  29262  5oalem7  29365  3oalem3  29369  pjrni  29407  mayete3i  29433  hmopex  29580  cnlnssadj  29785  adjbdln  29788  adjsslnop  29792  shatomistici  30066  hatomistici  30067  xrge0tsmsd  30620  primefldchr  30795  esumpcvgval  31237  hashf2  31243  insiga  31296  sigapisys  31314  sigaldsys  31318  sigapildsys  31321  sxbrsigalem0  31429  dya2icobrsiga  31434  sxbrsigalem1  31443  sxbrsigalem2  31444  eulerpartlemb  31526  chtvalz  31800  logdivsqrle  31821  bnj1398  32204  bnj1498  32231  erdszelem9  32344  erdsze2lem2  32349  kur14lem9  32359  ptpconn  32378  iinllyconn  32399  cvmlift3  32473  mppsthm  32724  imagesset  33312  altxpsspw  33336  topjoin  33611  onsstopbas  33675  onsucconni  33683  onintopssconn  33686  onint1  33695  oninhaus  33696  bj-snglss  34180  bj-modssabl  34451  bj-rvecssmod  34466  bj-rvecssvec  34471  bj-rvecsscmod  34473  icoreunrn  34523  difunieq  34538  poimirlem8  34782  poimirlem18  34792  poimirlem21  34795  poimirlem22  34796  poimirlem31  34805  poimirlem32  34806  heiborlem3  34974  atssbase  36308  eldioph3b  39242  diophin  39249  diophun  39250  eldiophss  39251  isnumbasabl  39586  isnumbasgrp  39587  dfacbasgrp  39588  mon1psubm  39686  inintabss  39818  intimass  39879  inaex  40513  nzin  40530  unipwrVD  41046  unipwr  41047  supxrre3  41473  fsumiunss  41736  rrpsscn  41749  dvnmul  42108  dvnprodlem2  42112  stoweidlem34  42200  stirlinglem13  42252  fourierdlem20  42293  fourierdlem62  42334  fourierdlem83  42355  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fouriersw  42397  qndenserrnbllem  42460  sge0iunmptlemre  42578  nn0ssge0  42587  sge0isum  42590  sge0seq  42609  sge0reuz  42610  caragendifcl  42677  carageniuncllem2  42685  hoicvrrex  42719  smfaddlem1  42920  smfaddlem2  42921  mbfpsssmf  42940  smndex1basss  43975  ringssrng  44049  srhmsubc  44245  srhmsubcALTV  44263  lvecpsslmod  44460  aacllem  44800  amgmwlem  44801  amgmlemALT  44802
  Copyright terms: Public domain W3C validator