Theorem ssriv 3917

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900

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

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

This theorem is used by:  ssid  3935  ssv  3937  ssrab2  4008  difss  4075  inss1  4136  ssun1  4179  0ss  4353  difprsnss  4762  snsspw  4802  uniinOLD  4895  pwuni  4909  iuniin  4967  iunpwss  5070  relopabiOLD  5806  dmin  5900  dmrnssfld  5963  dmcoss  5964  dmcossOLD  5965  dminss  6155  imainss  6156  fvssunirn  6939  fviss  6985  opabresex2  7497  fvmptopab  7498  mapfoss  8902  fsetsspwxp  8903  mapsspm  8932  pmsspw  8933  uniixp  8977  pwfilem  9337  dffi3  9450  dfom3  9675  onwf  9867  tcrank  9928  hfuni  9951  djuss  10028  djuunxp  10029  djuun  10034  cardprclem  10087  alephsson  10206  ackbij1  10342  cardcf  10356  cfeq0  10361  dfacfin7  10504  hsmexlem6  10536  canthnum  10761  inaprc  10948  nqerf  11042  addnqf  11060  mulnqf  11061  dmrecnq  11080  reclem2pr  11160  wuncn  11282  zssre  12727  zsscn  12728  nnssz  12742  elq  13104  zssq  13110  qssre  13113  ixxssixx  13517  iooval2  13536  ioossre  13565  rge0ssre  13614  fzssz  13685  fz1ssnn  13716  fzssuz  13726  fzssp1  13728  uzdisj  13758  fz0ssnn0  13783  nn0disj  13805  fzossfz  13840  fzouzsplit  13856  fzo0ssnn0  13908  uzrdgfni  14128  seqcoll  14636  wrdexb  14697  fclim  15749  isercolllem3  15863  climcnds  16049  divcnv  16051  harmonic  16057  bitsss  16625  prmssnn  16880  prmssuz2  16901  maxprmfct  16914  1arith  17134  4sqlem19  17170  vdwlem12  17199  restsspw  17631  mremre  17803  mreacs  17861  isfunc  18068  homarel  18240  ledm  18793  lern  18794  chnexg  18821  smndex1basss  19133  sgrpssmgm  19161  mndsssgrp  19162  prdsgrpd  19289  prdsinvgd  19290  symgpssefmnd  19640  symgsubmefmndALT  19647  pgrpsubgsymg  19653  symgtrf  19713  odf1o2  19817  sylow3lem3  19873  sylow3lem6  19876  oppglsm  19886  efgsfo  19983  0frgp  20023  prdscmnd  20105  prdsabld  20106  dprdssv  20262  dprdres  20274  prdsrngd  20428  ringssrng  20545  prdsringd  20580  prdscrngd  20581  unitss  20636  subrngint  20842  subrgint  20877  srhmsubc  20962  subdrgint  21090  sdrgint  21091  primefld  21092  lssintcl  21269  prdslmodd  21274  cnsubmlem  21751  cnsubglem  21752  cnsubdrglem  21754  cnmsubglem  21766  xrge0subm  21779  zringunit  21802  zringlpir  21803  znf1o  21887  ocvss  22006  dsmmsubg  22079  dsmmlss  22080  lbslinds  22169  unitg  23315  cldss2  23378  indiscld  23439  iscldtop  23443  llyssnlly  23827  llyidm  23837  nllyidm  23838  toplly  23839  hauslly  23841  lly1stc  23845  dissnref  23877  txindis  23983  pthaus  23987  ptcmpfi  24162  ufinffr  24278  cnflf2  24352  flimfcls  24375  alexsubALTlem3  24398  ptcmplem1  24401  ptcmpg  24406  prdstmdd  24473  prdstgpd  24474  ust0  24569  prdsms  24880  qdensere  25118  blssioo  25144  tgioo  25145  xrtgioo  25156  xrsmopn  25162  zdis  25166  reperflem  25168  xrge0gsumle  25183  xrge0tsms  25184  icopnfhmeo  25294  bndth  25309  voliunlem2  25902  voliunlem3  25903  vitali  25964  ismbf3d  26005  itg2seq  26093  limccl  26225  limcresi  26235  dvef  26330  aasscn  26671  qssaa  26678  aannenlem2  26686  aannenlem3  26687  ulmcn  26756  mtestbdd  26762  iblulm  26764  reeff1o  26804  reefgim  26807  efifo  26905  dfrelog  26923  relogf1o  26924  logdmss  27000  logcn  27005  dvloglem  27006  logf1o2  27008  dvlog  27009  dvlog2lem  27010  dvlog2  27011  logtayl  27018  cxpcn  27103  cxpcn2  27104  cxpcn3  27106  resqrtcn  27107  efrlim  27327  dfef2  27328  cxp2lim  27334  basellem3  27440  basellem4  27441  sqff1o  27539  dchrmhm  27598  chtppilim  27832  chto1lb  27835  chpchtlim  27836  chpo1ub  27837  dchrisumlema  27845  selberg2lem  27907  selberg3lem2  27915  pntrsumo1  27922  pnt2  27970  pnt  27971  madef  28252  oniso  28687  bdayn0sf1o  28786  dfnns2  28788  axcontlem2  29573  usgrexmplef  29870  griedg0ssusgr  29876  nbgrssvtx  29953  nbgrssovtx  29972  uvtxssvtx  30001  rgrusgrprc  30200  clwlkswks  30393  wwlkssswrd  30481  wwlkssswwlksn  30485  wspthsswwlkn  30537  wspthsswwlknon  30540  clwwlksclwwlkn  30652  phrel  31447  bnrel  31499  hlrel  31522  shex  31844  chsssh  31857  hhssnv  31896  choc1  31959  shunssi  32000  shsleji  32002  shsub1i  32004  shsub2i  32005  shsidmi  32016  omlsii  32035  spanuni  32176  spansni  32189  5oalem7  32292  3oalem3  32296  pjrni  32334  mayete3i  32360  hmopex  32507  cnlnssadj  32712  adjbdln  32715  adjsslnop  32719  shatomistici  32993  hatomistici  32994  xrge0tsmsd  33704  primefldchr  33933  1fldgenq  33954  zringidom  34153  esumpcvgval  34780  hashf2  34786  insiga  34840  sigapisys  34858  sigaldsys  34862  sigapildsys  34865  sxbrsigalem0  34973  dya2icobrsiga  34978  sxbrsigalem1  34987  sxbrsigalem2  34988  eulerpartlemb  35070  chtvalz  35328  logdivsqrle  35349  bnj1398  35734  bnj1498  35761  scottidm  35841  fineqvacALT  35885  fineqvhfbregs  35906  erdszelem9  36131  erdsze2lem2  36136  kur14lem9  36146  ptpconn  36165  iinllyconn  36186  cvmlift3  36260  mppsthm  36511  imagesset  36895  altxpsspw  36920  topjoin  37331  onsstopbas  37395  onsucconni  37403  onintopssconn  37406  onint1  37415  oninhaus  37416  ttcid  37458  dfttc4lem2  37495  dfttc4  37496  bj-snglss  38061  bj-imdirco  38303  bj-modssabl  38393  bj-rvecssmod  38409  bj-rvecssvec  38414  bj-rvecsscmod  38416  icoreunrn  38474  difunieq  38489  poimirlem8  38738  poimirlem18  38748  poimirlem21  38751  poimirlem22  38752  poimirlem31  38761  poimirlem32  38762  heiborlem3  38939  disjsssrels  40060  atssbase  40539  readvrec2  43605  eldioph3b  43969  diophin  43976  diophun  43977  eldiophss  43978  isnumbasabl  44300  isnumbasgrp  44301  dfacbasgrp  44302  mon1psubm  44393  omssrncard  44733  inintabss  44771  intimass  44846  inaex  45473  nzin  45494  unipwrVD  46005  unipwr  46006  omsshf  46217  supxrre3  46542  fsumiunss  46792  rrpsscn  46805  dvnmul  47158  dvnprodlem2  47162  stoweidlem34  47249  stirlinglem13  47301  fourierdlem20  47342  fourierdlem62  47383  fourierdlem83  47404  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fouriersw  47446  qndenserrnbllem  47509  sge0iunmptlemre  47630  nn0ssge0  47639  sge0isum  47642  sge0seq  47661  sge0reuz  47662  caragendifcl  47729  carageniuncllem2  47737  hoicvrrex  47771  smfaddlem1  47978  smfaddlem2  47979  mbfpsssmf  47998  wrddun2  48105  chndun2  48110  chnrun2  48115  clnbgrssvtx  49134  srhmsubcALTV  49627  lvecpsslmod  49824  thincssc  50764  aacllem  51219  amgmwlem  51267  amgmlemALT  51268