Theorem ssriv 3912

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		df-ss 3896	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1831	1 ⊢ 𝐴 ⊆ 𝐵

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ss 3896

This theorem is used by:  ssid  3930  ssv  3932  ssrab2  4005  difss  4072  inss1  4133  ssun1  4176  0ss  4349  difprsnss  4758  snsspw  4798  uniinOLD  4891  pwuni  4905  iuniin  4963  iunpwss  5066  relopabi  5799  dmin  5892  dmrnssfld  5955  dmcoss  5956  dmcossOLD  5957  dminss  6142  imainss  6143  fvssunirn  6916  fviss  6962  opabresex2  7474  fvmptopab  7475  mapfoss  8877  fsetsspwxp  8878  mapsspm  8907  pmsspw  8908  uniixp  8952  pwfilem  9312  dffi3  9426  dfom3  9651  onwf  9843  tcrank  9904  hfuni  9927  djuss  10004  djuunxp  10005  djuun  10010  cardprclem  10063  alephsson  10182  ackbij1  10318  cardcf  10332  cfeq0  10337  dfacfin7  10480  hsmexlem6  10512  canthnum  10737  inaprc  10924  nqerf  11018  addnqf  11036  mulnqf  11037  dmrecnq  11056  reclem2pr  11136  wuncn  11258  zssre  12703  zsscn  12704  nnssz  12718  elq  13080  zssq  13086  qssre  13089  ixxssixx  13493  iooval2  13512  ioossre  13541  rge0ssre  13590  fzssz  13661  fz1ssnn  13692  fzssuz  13702  fzssp1  13704  uzdisj  13734  fz0ssnn0  13759  nn0disj  13781  fzossfz  13816  fzouzsplit  13832  fzo0ssnn0  13884  uzrdgfni  14104  seqcoll  14612  wrdexb  14673  fclim  15725  isercolllem3  15839  climcnds  16025  divcnv  16027  harmonic  16033  bitsss  16601  prmssnn  16856  prmssuz2  16877  maxprmfct  16890  1arith  17110  4sqlem19  17146  vdwlem12  17175  restsspw  17607  mremre  17779  mreacs  17837  isfunc  18044  homarel  18216  ledm  18769  lern  18770  chnexg  18797  smndex1basss  19109  sgrpssmgm  19137  mndsssgrp  19138  prdsgrpd  19265  prdsinvgd  19266  symgpssefmnd  19615  symgsubmefmndALT  19622  pgrpsubgsymg  19628  symgtrf  19688  odf1o2  19792  sylow3lem3  19848  sylow3lem6  19851  oppglsm  19861  efgsfo  19958  0frgp  19998  prdscmnd  20080  prdsabld  20081  dprdssv  20237  dprdres  20249  prdsrngd  20403  ringssrng  20520  prdsringd  20555  prdscrngd  20556  unitss  20611  subrngint  20817  subrgint  20852  srhmsubc  20937  subdrgint  21065  sdrgint  21066  primefld  21067  lssintcl  21244  prdslmodd  21249  cnsubmlem  21726  cnsubglem  21727  cnsubdrglem  21729  cnmsubglem  21741  xrge0subm  21754  zringunit  21777  zringlpir  21778  znf1o  21862  ocvss  21981  dsmmsubg  22054  dsmmlss  22055  lbslinds  22144  unitg  23290  cldss2  23353  indiscld  23414  iscldtop  23418  llyssnlly  23802  llyidm  23812  nllyidm  23813  toplly  23814  hauslly  23816  lly1stc  23820  dissnref  23852  txindis  23958  pthaus  23962  ptcmpfi  24137  ufinffr  24253  cnflf2  24327  flimfcls  24350  alexsubALTlem3  24373  ptcmplem1  24376  ptcmpg  24381  prdstmdd  24448  prdstgpd  24449  ust0  24544  prdsms  24855  qdensere  25093  blssioo  25119  tgioo  25120  xrtgioo  25131  xrsmopn  25137  zdis  25141  reperflem  25143  xrge0gsumle  25158  xrge0tsms  25159  icopnfhmeo  25269  bndth  25284  voliunlem2  25877  voliunlem3  25878  vitali  25939  ismbf3d  25980  itg2seq  26068  limccl  26200  limcresi  26210  dvef  26305  aasscn  26646  qssaa  26653  aannenlem2  26661  aannenlem3  26662  ulmcn  26731  mtestbdd  26737  iblulm  26739  reeff1o  26779  reefgim  26782  efifo  26880  dfrelog  26898  relogf1o  26899  logdmss  26975  logcn  26980  dvloglem  26981  logf1o2  26983  dvlog  26984  dvlog2lem  26985  dvlog2  26986  logtayl  26993  cxpcn  27078  cxpcn2  27079  cxpcn3  27081  resqrtcn  27082  efrlim  27302  dfef2  27303  cxp2lim  27309  basellem3  27415  basellem4  27416  sqff1o  27514  dchrmhm  27573  chtppilim  27807  chto1lb  27810  chpchtlim  27811  chpo1ub  27812  dchrisumlema  27820  selberg2lem  27882  selberg3lem2  27890  pntrsumo1  27897  pnt2  27945  pnt  27946  madef  28227  oniso  28662  bdayn0sf1o  28761  dfnns2  28763  axcontlem2  29548  usgrexmplef  29845  griedg0ssusgr  29851  nbgrssvtx  29928  nbgrssovtx  29947  uvtxssvtx  29976  rgrusgrprc  30175  clwlkswks  30368  wwlkssswrd  30456  wwlkssswwlksn  30460  wspthsswwlkn  30512  wspthsswwlknon  30515  clwwlksclwwlkn  30627  phrel  31422  bnrel  31474  hlrel  31497  shex  31819  chsssh  31832  hhssnv  31871  choc1  31934  shunssi  31975  shsleji  31977  shsub1i  31979  shsub2i  31980  shsidmi  31991  omlsii  32010  spanuni  32151  spansni  32164  5oalem7  32267  3oalem3  32271  pjrni  32309  mayete3i  32335  hmopex  32482  cnlnssadj  32687  adjbdln  32690  adjsslnop  32694  shatomistici  32968  hatomistici  32969  xrge0tsmsd  33680  primefldchr  33909  1fldgenq  33930  zringidom  34129  esumpcvgval  34756  hashf2  34762  insiga  34816  sigapisys  34834  sigaldsys  34838  sigapildsys  34841  sxbrsigalem0  34949  dya2icobrsiga  34954  sxbrsigalem1  34963  sxbrsigalem2  34964  eulerpartlemb  35046  chtvalz  35304  logdivsqrle  35325  bnj1398  35710  bnj1498  35737  r1omfi  35782  fineqvacALT  35841  erdszelem9  36050  erdsze2lem2  36055  kur14lem9  36065  ptpconn  36084  iinllyconn  36105  cvmlift3  36179  mppsthm  36430  imagesset  36809  altxpsspw  36834  topjoin  37245  onsstopbas  37309  onsucconni  37317  onintopssconn  37320  onint1  37329  oninhaus  37330  ttcid  37372  dfttc4lem2  37409  dfttc4  37410  bj-snglss  37975  bj-imdirco  38204  bj-modssabl  38294  bj-rvecssmod  38310  bj-rvecssvec  38315  bj-rvecsscmod  38317  icoreunrn  38375  difunieq  38390  poimirlem8  38639  poimirlem18  38649  poimirlem21  38652  poimirlem22  38653  poimirlem31  38662  poimirlem32  38663  heiborlem3  38840  disjsssrels  39961  atssbase  40440  readvrec2  43505  eldioph3b  43869  diophin  43876  diophun  43877  eldiophss  43878  isnumbasabl  44201  isnumbasgrp  44202  dfacbasgrp  44203  mon1psubm  44294  omssrncard  44634  inintabss  44672  intimass  44747  inaex  45374  nzin  45395  unipwrVD  45907  unipwr  45908  omsshf  46115  supxrre3  46430  fsumiunss  46680  rrpsscn  46693  dvnmul  47046  dvnprodlem2  47050  stoweidlem34  47137  stirlinglem13  47189  fourierdlem20  47230  fourierdlem62  47271  fourierdlem83  47292  fourierdlem101  47310  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fouriersw  47334  qndenserrnbllem  47397  sge0iunmptlemre  47518  nn0ssge0  47527  sge0isum  47530  sge0seq  47549  sge0reuz  47550  caragendifcl  47617  carageniuncllem2  47625  hoicvrrex  47659  smfaddlem1  47866  smfaddlem2  47867  mbfpsssmf  47886  wrddun2  47993  chndun2  47998  chnrun2  48003  clnbgrssvtx  49022  srhmsubcALTV  49515  lvecpsslmod  49712  thincssc  50652  aacllem  51107  amgmwlem  51155  amgmlemALT  51156