Theorem ssriv 3944

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3908

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 3925

This theorem is used by:  ssid  3962  ssv  3964  ssrab2  4037  difss  4093  ssun1  4134  inss1  4192  0ss  4360  difprsnss  4772  snsspw  4814  uniinOLD  4902  pwuni  4916  iuniin  4974  iunpwss  5078  relopabi  5814  dmin  5906  dmrnssfld  5969  dmcoss  5970  dmcossOLD  5971  dminss  6155  imainss  6156  fvssunirn  6919  fviss  6965  opabresex2  7477  fvmptopab  7478  mapfoss  8858  fsetsspwxp  8859  mapsspm  8883  pmsspw  8884  uniixp  8928  pwfilem  9287  dffi3  9401  dfom3  9626  onwf  9812  tcrank  9866  djuss  9925  djuunxp  9926  djuun  9931  cardprclem  9984  alephsson  10103  ackbij1  10239  cardcf  10253  cfeq0  10258  dfacfin7  10401  hsmexlem6  10433  canthnum  10652  inaprc  10839  nqerf  10933  addnqf  10951  mulnqf  10952  dmrecnq  10971  reclem2pr  11051  wuncn  11173  zssre  12616  zsscn  12617  nnssz  12631  elq  12992  zssq  12998  qssre  13001  ixxssixx  13404  iooval2  13423  ioossre  13452  rge0ssre  13501  fzssz  13572  fz1ssnn  13602  fzssuz  13612  fzssp1  13614  uzdisj  13644  fz0ssnn0  13669  nn0disj  13691  fzossfz  13726  fzouzsplit  13742  fzo0ssnn0  13794  uzrdgfni  14014  seqcoll  14521  wrdexb  14582  fclim  15630  isercolllem3  15744  climcnds  15931  divcnv  15933  harmonic  15939  bitsss  16509  prmssnn  16759  prmssuz2  16780  maxprmfct  16793  1arith  17012  4sqlem19  17048  vdwlem12  17077  restsspw  17509  mremre  17681  mreacs  17739  isfunc  17946  homarel  18118  ledm  18671  lern  18672  chnexg  18699  smndex1basss  18998  sgrpssmgm  19026  mndsssgrp  19027  prdsgrpd  19147  prdsinvgd  19148  symgpssefmnd  19497  symgsubmefmndALT  19504  pgrpsubgsymg  19510  symgtrf  19570  odf1o2  19674  sylow3lem3  19730  sylow3lem6  19733  oppglsm  19743  efgsfo  19840  0frgp  19880  prdscmnd  19962  prdsabld  19963  dprdssv  20119  dprdres  20131  prdsrngd  20285  ringssrng  20401  prdsringd  20435  prdscrngd  20436  unitss  20491  subrngint  20696  subrgint  20731  srhmsubc  20816  subdrgint  20943  sdrgint  20944  primefld  20945  lssintcl  21122  prdslmodd  21127  cnsubmlem  21602  cnsubglem  21603  cnsubdrglem  21605  cnmsubglem  21617  xrge0subm  21630  zringunit  21653  zringlpir  21654  znf1o  21738  ocvss  21857  dsmmsubg  21930  dsmmlss  21931  lbslinds  22020  unitg  23161  cldss2  23224  indiscld  23285  iscldtop  23289  llyssnlly  23672  llyidm  23682  nllyidm  23683  toplly  23684  hauslly  23686  lly1stc  23690  dissnref  23722  txindis  23828  pthaus  23832  ptcmpfi  24007  ufinffr  24123  cnflf2  24197  flimfcls  24220  alexsubALTlem3  24243  ptcmplem1  24246  ptcmpg  24251  prdstmdd  24318  prdstgpd  24319  ust0  24414  prdsms  24725  qdensere  24963  blssioo  24989  tgioo  24990  xrtgioo  25001  xrsmopn  25007  zdis  25011  reperflem  25013  xrge0gsumle  25028  xrge0tsms  25029  icopnfhmeo  25139  bndth  25154  voliunlem2  25747  voliunlem3  25748  vitali  25809  ismbf3d  25850  itg2seq  25938  limccl  26071  limcresi  26081  dvef  26176  aasscn  26516  qssaa  26522  aannenlem2  26529  aannenlem3  26530  ulmcn  26599  mtestbdd  26605  iblulm  26607  reeff1o  26647  reefgim  26650  efifo  26749  dfrelog  26767  relogf1o  26768  logdmss  26844  logcn  26849  dvloglem  26850  logf1o2  26852  dvlog  26853  dvlog2lem  26854  dvlog2  26855  logtayl  26862  cxpcn  26947  cxpcn2  26948  cxpcn3  26950  resqrtcn  26951  efrlim  27171  dfef2  27172  cxp2lim  27178  basellem3  27284  basellem4  27285  sqff1o  27383  dchrmhm  27442  chtppilim  27676  chto1lb  27679  chpchtlim  27680  chpo1ub  27681  dchrisumlema  27689  selberg2lem  27751  selberg3lem2  27759  pntrsumo1  27766  pnt2  27814  pnt  27815  madef  28066  oniso  28501  bdayn0sf1o  28600  dfnns2  28602  axcontlem2  29352  usgrexmplef  29646  griedg0ssusgr  29652  nbgrssvtx  29729  nbgrssovtx  29748  uvtxssvtx  29777  rgrusgrprc  29976  clwlkswks  30162  wwlkssswrd  30248  wwlkssswwlksn  30252  wspthsswwlkn  30304  wspthsswwlknon  30307  clwwlksclwwlkn  30419  phrel  31204  bnrel  31256  hlrel  31279  shex  31601  chsssh  31614  hhssnv  31653  choc1  31716  shunssi  31757  shsleji  31759  shsub1i  31761  shsub2i  31762  shsidmi  31773  omlsii  31792  spanuni  31933  spansni  31946  5oalem7  32049  3oalem3  32053  pjrni  32091  mayete3i  32117  hmopex  32264  cnlnssadj  32469  adjbdln  32472  adjsslnop  32476  shatomistici  32750  hatomistici  32751  xrge0tsmsd  33424  primefldchr  33653  1fldgenq  33674  zringidom  33872  esumpcvgval  34499  hashf2  34505  insiga  34559  sigapisys  34577  sigaldsys  34581  sigapildsys  34584  sxbrsigalem0  34693  dya2icobrsiga  34698  sxbrsigalem1  34707  sxbrsigalem2  34708  eulerpartlemb  34790  chtvalz  35048  logdivsqrle  35069  bnj1398  35454  bnj1498  35481  r1omfi  35524  fineqvacALT  35554  erdszelem9  35712  erdsze2lem2  35717  kur14lem9  35727  ptpconn  35746  iinllyconn  35767  cvmlift3  35841  mppsthm  36092  imagesset  36466  altxpsspw  36490  topjoin  36917  onsstopbas  36981  onsucconni  36989  onintopssconn  36992  onint1  37001  oninhaus  37002  ttcid  37044  dfttc4lem2  37081  dfttc4  37082  bj-snglss  37647  bj-imdirco  37875  bj-modssabl  37965  bj-rvecssmod  37981  bj-rvecssvec  37986  bj-rvecsscmod  37988  icoreunrn  38046  difunieq  38061  poimirlem8  38320  poimirlem18  38330  poimirlem21  38333  poimirlem22  38334  poimirlem31  38343  poimirlem32  38344  heiborlem3  38505  disjsssrels  39626  atssbase  40105  readvrec2  43163  eldioph3b  43537  diophin  43544  diophun  43545  eldiophss  43546  isnumbasabl  43874  isnumbasgrp  43875  dfacbasgrp  43876  mon1psubm  43967  omssrncard  44307  inintabss  44345  intimass  44421  inaex  45048  nzin  45069  unipwrVD  45581  unipwr  45582  supxrre3  46082  fsumiunss  46332  rrpsscn  46345  dvnmul  46698  dvnprodlem2  46702  stoweidlem34  46789  stirlinglem13  46841  fourierdlem20  46882  fourierdlem62  46923  fourierdlem83  46944  fourierdlem101  46962  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fouriersw  46986  qndenserrnbllem  47049  sge0iunmptlemre  47170  nn0ssge0  47179  sge0isum  47182  sge0seq  47201  sge0reuz  47202  caragendifcl  47269  carageniuncllem2  47277  hoicvrrex  47311  smfaddlem1  47518  smfaddlem2  47519  mbfpsssmf  47538  clnbgrssvtx  48637  srhmsubcALTV  49131  lvecpsslmod  49328  thincssc  50243  aacllem  50662  amgmwlem  50691  amgmlemALT  50692