Theorem ssriv 3971

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

Step	Hyp	Ref	Expression
1		dfss2 3955	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1800	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  ssid  3989  ssv  3991  difss  4108  ssun1  4148  inss1  4205  0ss  4350  difprsnss  4732  snsspw  4775  uniin  4862  pwuni  4875  iuniin  4931  iunpwss  5029  pwunssOLD  5455  relopabi  5694  dmin  5780  dmrnssfld  5841  dmcoss  5842  dminss  6010  imainss  6011  fviss  6741  mapsspm  8440  pmsspw  8441  uniixp  8485  pwfilem  8818  dffi3  8895  dfom3  9110  onwf  9259  tcrank  9313  djuss  9349  djuunxp  9350  djuun  9355  cardprclem  9408  alephsson  9526  ackbij1  9660  cardcf  9674  cfeq0  9678  dfacfin7  9821  hsmexlem6  9853  canthnum  10071  inaprc  10258  nqerf  10352  addnqf  10370  mulnqf  10371  dmrecnq  10390  reclem2pr  10470  wuncn  10592  zssre  11989  zsscn  11990  nnssz  12003  elq  12351  zssq  12356  qssre  12359  ixxssixx  12753  iooval2  12772  ioossre  12799  rge0ssre  12845  fzssz  12910  fz1ssnn  12939  fzssuz  12949  fzssp1  12951  uzdisj  12981  fz0ssnn0  13003  nn0disj  13024  fzossfz  13057  fzouzsplit  13073  fzo0ssnn0  13119  uzrdgfni  13327  seqcoll  13823  wrdexgOLD  13873  wrdexb  13874  fclim  14910  isercolllem3  15023  climcnds  15206  divcnv  15208  harmonic  15214  bitsss  15775  prmssnn  16020  maxprmfct  16053  1arith  16263  4sqlem19  16299  vdwlem12  16328  restsspw  16705  mremre  16875  mreacs  16929  isfunc  17134  homarel  17296  ledm  17834  lern  17835  smndex1basss  18070  sgrpssmgm  18098  mndsssgrp  18099  prdsgrpd  18209  prdsinvgd  18210  symgpssefmnd  18524  symgsubmefmndALT  18531  pgrpsubgsymg  18537  symgtrf  18597  odf1o2  18698  sylow3lem3  18754  sylow3lem6  18757  oppglsm  18767  efgsfo  18865  0frgp  18905  prdscmnd  18981  prdsabld  18982  dprdssv  19138  dprdres  19150  prdsringd  19362  prdscrngd  19363  unitss  19410  subrgint  19557  subdrgint  19582  sdrgint  19583  primefld  19584  lssintcl  19736  prdslmodd  19741  xrge0subm  20586  cnsubmlem  20593  cnsubglem  20594  cnsubdrglem  20596  cnmsubglem  20608  zringunit  20635  zringlpir  20636  znf1o  20698  zntoslem  20703  ocvss  20814  dsmmsubg  20887  dsmmlss  20888  lbslinds  20977  unitg  21575  cldss2  21638  indiscld  21699  iscldtop  21703  llyssnlly  22086  llyidm  22096  nllyidm  22097  toplly  22098  hauslly  22100  lly1stc  22104  dissnref  22136  txindis  22242  pthaus  22246  ptcmpfi  22421  ufinffr  22537  cnflf2  22611  flimfcls  22634  alexsubALTlem3  22657  ptcmplem1  22660  ptcmpg  22665  prdstmdd  22732  prdstgpd  22733  ust0  22828  prdsms  23141  qdensere  23378  blssioo  23403  tgioo  23404  xrtgioo  23414  xrsmopn  23420  zdis  23424  reperflem  23426  xrge0gsumle  23441  xrge0tsms  23442  icopnfhmeo  23547  bndth  23562  voliunlem2  24152  voliunlem3  24153  vitali  24214  ismbf3d  24255  itg2seq  24343  limccl  24473  limcresi  24483  dvef  24577  aasscn  24907  qssaa  24913  aannenlem2  24918  aannenlem3  24919  ulmcn  24987  mtestbdd  24993  iblulm  24995  reeff1o  25035  reefgim  25038  efifo  25131  dfrelog  25149  relogf1o  25150  logdmss  25225  logcn  25230  dvloglem  25231  logf1o2  25233  dvlog  25234  dvlog2lem  25235  dvlog2  25236  logtayl  25243  cxpcn  25326  cxpcn2  25327  cxpcn3  25329  resqrtcn  25330  efrlim  25547  dfef2  25548  cxp2lim  25554  basellem3  25660  basellem4  25661  sqff1o  25759  dchrmhm  25817  chtppilim  26051  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  dchrisumlema  26064  selberg2lem  26126  selberg3lem2  26134  pntrsumo1  26141  pnt2  26189  pnt  26190  axcontlem2  26751  usgrexmplef  27041  griedg0ssusgr  27047  nbgrssvtx  27124  nbgrssovtx  27143  uvtxssvtx  27172  rgrusgrprc  27371  clwlkswks  27557  wwlkssswrd  27640  wwlkssswwlksn  27644  wspthsswwlkn  27697  wspthsswwlknon  27700  clwwlksclwwlkn  27809  phrel  28592  bnrel  28644  hlrel  28667  shex  28989  chsssh  29002  hhssnv  29041  choc1  29104  shunssi  29145  shsleji  29147  shsub1i  29149  shsub2i  29150  shsidmi  29161  omlsii  29180  spanuni  29321  spansni  29334  5oalem7  29437  3oalem3  29441  pjrni  29479  mayete3i  29505  hmopex  29652  cnlnssadj  29857  adjbdln  29860  adjsslnop  29864  shatomistici  30138  hatomistici  30139  xrge0tsmsd  30692  primefldchr  30867  esumpcvgval  31337  hashf2  31343  insiga  31396  sigapisys  31414  sigaldsys  31418  sigapildsys  31421  sxbrsigalem0  31529  dya2icobrsiga  31534  sxbrsigalem1  31543  sxbrsigalem2  31544  eulerpartlemb  31626  chtvalz  31900  logdivsqrle  31921  bnj1398  32306  bnj1498  32333  erdszelem9  32446  erdsze2lem2  32451  kur14lem9  32461  ptpconn  32480  iinllyconn  32501  cvmlift3  32575  mppsthm  32826  imagesset  33414  altxpsspw  33438  topjoin  33713  onsstopbas  33777  onsucconni  33785  onintopssconn  33788  onint1  33797  oninhaus  33798  bj-snglss  34285  bj-modssabl  34565  bj-rvecssmod  34580  bj-rvecssvec  34585  bj-rvecsscmod  34587  icoreunrn  34643  difunieq  34658  poimirlem8  34915  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem31  34938  poimirlem32  34939  heiborlem3  35106  atssbase  36441  eldioph3b  39411  diophin  39418  diophun  39419  eldiophss  39420  isnumbasabl  39755  isnumbasgrp  39756  dfacbasgrp  39757  mon1psubm  39855  inintabss  39987  intimass  40048  inaex  40682  nzin  40699  unipwrVD  41215  unipwr  41216  supxrre3  41642  fsumiunss  41905  rrpsscn  41918  dvnmul  42277  dvnprodlem2  42281  stoweidlem34  42368  stirlinglem13  42420  fourierdlem20  42461  fourierdlem62  42502  fourierdlem83  42523  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fouriersw  42565  qndenserrnbllem  42628  sge0iunmptlemre  42746  nn0ssge0  42755  sge0isum  42758  sge0seq  42777  sge0reuz  42778  caragendifcl  42845  carageniuncllem2  42853  hoicvrrex  42887  smfaddlem1  43088  smfaddlem2  43089  mbfpsssmf  43108  ringssrng  44200  srhmsubc  44396  srhmsubcALTV  44414  lvecpsslmod  44611  aacllem  44951  amgmwlem  44952  amgmlemALT  44953