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

Theorem ssriv 3605
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
StepHypRef Expression
1 dfss2 3589 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 ssriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1725 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3579  df-ss 3586
This theorem is referenced by:  ssid  3622  ssv  3623  difss  3735  ssun1  3774  inss1  3831  0ss  3970  difprsnss  4327  snsspw  4373  uniin  4455  pwuni  4472  iuniin  4529  iunpwss  4616  pwunss  5017  relopabi  5243  dmin  5330  dmrnssfld  5382  dmcoss  5383  dminss  5545  imainss  5546  fviss  6254  mapsspm  7888  pmsspw  7889  uniixp  7928  pwfilem  8257  dffi3  8334  dfom3  8541  onwf  8690  tcrank  8744  cardprclem  8802  alephsson  8920  ackbij1  9057  cardcf  9071  cfeq0  9075  dfacfin7  9218  hsmexlem6  9250  canthnum  9468  inaprc  9655  nqerf  9749  addnqf  9767  mulnqf  9768  dmrecnq  9787  reclem2pr  9867  wuncn  9988  zssre  11381  zsscn  11382  nnssz  11394  elq  11787  zssq  11792  qssre  11795  rpssre  11840  ixxssixx  12186  iooval2  12205  ioossre  12232  rge0ssre  12277  fzssz  12340  fz1ssnn  12369  fzssuz  12379  fzssp1  12381  uzdisj  12409  fz0ssnn0  12431  nn0disj  12451  fzossfz  12484  fzouzsplit  12499  fzossnn  12512  fzo0ssnn0  12544  fzo0ssnn0OLD  12545  uzrdgfni  12752  seqcoll  13243  wrdexg  13310  wrdexb  13311  fclim  14278  isercolllem3  14391  isercoll  14392  climcnds  14577  divcnv  14579  harmonic  14585  fprodge0  14718  bitsss  15142  prmssnn  15384  maxprmfct  15415  prminf  15613  prmreclem3  15616  1arithlem1  15621  1arith  15625  4sqlem19  15661  vdwlem12  15690  restsspw  16086  xpsc0  16214  xpsc1  16215  mremre  16258  mreacs  16313  isfunc  16518  homarel  16680  ledm  17218  lern  17219  sgrpssmgm  17414  mndsssgrp  17415  prdsgrpd  17519  prdsinvgd  17520  symgtrf  17883  odf1o2  17982  sylow3lem3  18038  sylow3lem6  18041  oppglsm  18051  efgsfo  18146  0frgp  18186  prdscmnd  18258  prdsabld  18259  dprdssv  18409  dprdres  18421  ablfac1b  18463  prdsringd  18606  prdscrngd  18607  unitss  18654  subrgint  18796  lssintcl  18958  prdslmodd  18963  xrge0subm  19781  cnsubmlem  19788  cnsubglem  19789  cnsubdrglem  19791  cnmsubglem  19803  zringunit  19830  zringlpir  19831  znf1o  19894  zntoslem  19899  ocvss  20008  dsmmsubg  20081  dsmmlss  20082  lbslinds  20166  unitg  20765  cldss2  20828  indiscld  20889  toponmre  20891  iscldtop  20893  1stcfb  21242  llyssnlly  21275  llyidm  21285  nllyidm  21286  toplly  21287  hauslly  21289  lly1stc  21293  dissnref  21325  1stckgenlem  21350  txindis  21431  pthaus  21435  ptcmpfi  21610  ufinffr  21727  cnflf2  21801  flimfcls  21824  alexsubALTlem3  21847  ptcmplem1  21850  ptcmpg  21855  prdstmdd  21921  prdstgpd  21922  ust0  22017  prdsms  22330  qdensere  22567  blssioo  22592  tgioo  22593  xrtgioo  22603  xrsmopn  22609  zdis  22613  reperflem  22615  xrge0gsumle  22630  xrge0tsms  22631  icopnfhmeo  22736  bndth  22751  ovoliunlem1  23264  ovoliun2  23268  ovolicc2lem4  23282  voliunlem2  23313  voliunlem3  23314  uniioovol  23341  uniioombllem4  23348  vitali  23376  ismbf3d  23415  itg2seq  23503  limccl  23633  limcresi  23643  dvef  23737  aasscn  24067  qssaa  24073  aannenlem2  24078  aannenlem3  24079  ulmcn  24147  mtestbdd  24153  iblulm  24155  reeff1o  24195  reefgim  24198  efifo  24287  dfrelog  24306  relogf1o  24307  logdmss  24382  logcn  24387  dvloglem  24388  logf1o2  24390  dvlog  24391  dvlog2lem  24392  dvlog2  24393  logtayl  24400  cxpcn  24480  cxpcn2  24481  cxpcn3  24483  resqrtcn  24484  efrlim  24690  dfef2  24691  cxp2lim  24697  wilthlem2  24789  wilthlem3  24790  basellem3  24803  basellem4  24804  prmdvdsfi  24827  vmaval  24833  mumul  24901  sqff1o  24902  musum  24911  fsumvma2  24933  dchrmhm  24960  chtppilim  25158  chto1lb  25161  chpchtlim  25162  chpo1ub  25163  dchrisumlema  25171  dchrmusum2  25177  dchrvmasum2lem  25179  dirith2  25211  mudivsum  25213  mulogsum  25215  mulog2sumlem2  25218  selberg2lem  25233  selberg3lem2  25241  pntrsumo1  25248  pnt2  25296  pnt  25297  axcontlem2  25839  usgrexmplef  26145  griedg0ssusgr  26151  uvtxassvtx  26284  rgrusgrprc  26479  clwlkswks  26666  wwlkssswrd  26741  wwlkssswwlksn  26745  wspthsswwlkn  26808  wspthsswwlknon  26811  clwwlkssclwwlksn  26886  phrel  27654  bnrel  27707  hlrel  27730  shex  28053  chsssh  28066  hhssnv  28105  choc1  28170  shunssi  28211  shsleji  28213  shsub1i  28215  shsub2i  28216  shsidmi  28227  omlsii  28246  spanuni  28387  spansni  28400  5oalem7  28503  3oalem3  28507  pjrni  28545  mayete3i  28571  hmopex  28718  cnlnssadj  28923  adjbdln  28926  adjsslnop  28930  shatomistici  29204  hatomistici  29205  xrge0tsmsd  29770  esumpcvgval  30125  hashf2  30131  insiga  30185  sigapisys  30203  sigaldsys  30207  sigapildsys  30210  sxbrsigalem0  30318  dya2icobrsiga  30323  sxbrsigalem1  30332  sxbrsigalem2  30333  eulerpartlemb  30415  chtvalz  30692  logdivsqrle  30713  bnj1398  31087  bnj1498  31114  erdszelem9  31166  erdsze2lem2  31171  kur14lem9  31181  ptpconn  31200  iinllyconn  31221  cvmlift3  31295  mppsthm  31461  imagesset  32044  altxpsspw  32068  topjoin  32344  onsstopbas  32412  onsucconni  32420  onintopssconn  32423  onint1  32432  oninhaus  32433  bj-snglss  32942  bj-modssabl  33122  icoreunrn  33187  poimirlem8  33397  poimirlem18  33407  poimirlem21  33410  poimirlem22  33411  poimirlem31  33420  poimirlem32  33421  heiborlem3  33592  atssbase  34403  eldioph3b  37154  diophin  37162  diophun  37163  eldiophss  37164  isnumbasabl  37502  isnumbasgrp  37503  dfacbasgrp  37504  mon1psubm  37610  inintabss  37710  intimass  37772  nzin  38343  unipwrVD  38893  unipwr  38894  supxrre3  39360  fsumiunss  39613  rrpsscn  39626  dvnmul  39927  dvnprodlem2  39931  stoweidlem34  40020  stirlinglem13  40072  fourierdlem20  40113  fourierdlem62  40154  fourierdlem83  40175  fourierdlem101  40193  fourierdlem103  40195  fourierdlem104  40196  fourierdlem111  40203  fouriersw  40217  qndenserrnbllem  40283  sge0iunmptlemre  40401  nn0ssge0  40410  sge0isum  40413  sge0seq  40432  sge0reuz  40433  caragendifcl  40497  carageniuncllem2  40505  hoicvrrex  40539  smfaddlem1  40740  smfaddlem2  40741  mbfpsssmf  40760  ringssrng  41651  srhmsubc  41847  srhmsubcALTV  41865  lvecpsslmod  42067  aacllem  42318  amgmwlem  42319  amgmlemALT  42320
  Copyright terms: Public domain W3C validator