Theorem ssriv 3934

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796

This theorem depends on definitions:  df-bi 207  df-ss 3915

This theorem is referenced by:  ssid  3953  ssv  3955  ssrab2  4029  difss  4085  ssun1  4127  inss1  4186  0ss  4349  difprsnss  4750  snsspw  4795  uniin  4882  pwuni  4896  iuniin  4954  iunpwss  5057  relopabi  5766  dmin  5855  dmrnssfld  5917  dmcoss  5918  dmcossOLD  5919  dminss  6105  imainss  6106  fvssunirn  6859  fviss  6905  opabresex2  7406  fvmptopab  7407  mapfoss  8782  fsetsspwxp  8783  mapsspm  8806  pmsspw  8807  uniixp  8851  pwfilem  9209  dffi3  9322  dfom3  9544  onwf  9730  tcrank  9784  djuss  9820  djuunxp  9821  djuun  9826  cardprclem  9879  alephsson  9998  ackbij1  10135  cardcf  10150  cfeq0  10154  dfacfin7  10297  hsmexlem6  10329  canthnum  10547  inaprc  10734  nqerf  10828  addnqf  10846  mulnqf  10847  dmrecnq  10866  reclem2pr  10946  wuncn  11068  zssre  12482  zsscn  12483  nnssz  12497  elq  12850  zssq  12856  qssre  12859  ixxssixx  13261  iooval2  13280  ioossre  13309  rge0ssre  13358  fzssz  13428  fz1ssnn  13457  fzssuz  13467  fzssp1  13469  uzdisj  13499  fz0ssnn0  13524  nn0disj  13546  fzossfz  13580  fzouzsplit  13596  fzo0ssnn0  13648  uzrdgfni  13867  seqcoll  14373  wrdexb  14434  fclim  15462  isercolllem3  15576  climcnds  15760  divcnv  15762  harmonic  15768  bitsss  16339  prmssnn  16589  maxprmfct  16622  1arith  16841  4sqlem19  16877  vdwlem12  16906  restsspw  17337  mremre  17508  mreacs  17566  isfunc  17773  homarel  17945  ledm  18498  lern  18499  chnexg  18526  smndex1basss  18815  sgrpssmgm  18843  mndsssgrp  18844  prdsgrpd  18965  prdsinvgd  18966  symgpssefmnd  19310  symgsubmefmndALT  19317  pgrpsubgsymg  19323  symgtrf  19383  odf1o2  19487  sylow3lem3  19543  sylow3lem6  19546  oppglsm  19556  efgsfo  19653  0frgp  19693  prdscmnd  19775  prdsabld  19776  dprdssv  19932  dprdres  19944  prdsrngd  20096  ringssrng  20206  prdsringd  20241  prdscrngd  20242  unitss  20296  subrngint  20477  subrgint  20512  srhmsubc  20597  subdrgint  20720  sdrgint  20721  primefld  20722  lssintcl  20899  prdslmodd  20904  cnsubmlem  21353  cnsubglem  21354  cnsubdrglem  21357  cnmsubglem  21369  xrge0subm  21382  zringunit  21405  zringlpir  21406  znf1o  21490  ocvss  21609  dsmmsubg  21682  dsmmlss  21683  lbslinds  21772  unitg  22883  cldss2  22946  indiscld  23007  iscldtop  23011  llyssnlly  23394  llyidm  23404  nllyidm  23405  toplly  23406  hauslly  23408  lly1stc  23412  dissnref  23444  txindis  23550  pthaus  23554  ptcmpfi  23729  ufinffr  23845  cnflf2  23919  flimfcls  23942  alexsubALTlem3  23965  ptcmplem1  23968  ptcmpg  23973  prdstmdd  24040  prdstgpd  24041  ust0  24136  prdsms  24447  qdensere  24685  blssioo  24711  tgioo  24712  xrtgioo  24723  xrsmopn  24729  zdis  24733  reperflem  24735  xrge0gsumle  24750  xrge0tsms  24751  icopnfhmeo  24869  bndth  24885  voliunlem2  25480  voliunlem3  25481  vitali  25542  ismbf3d  25583  itg2seq  25671  limccl  25804  limcresi  25814  dvef  25912  aasscn  26254  qssaa  26260  aannenlem2  26265  aannenlem3  26266  ulmcn  26336  mtestbdd  26342  iblulm  26344  reeff1o  26385  reefgim  26388  efifo  26484  dfrelog  26502  relogf1o  26503  logdmss  26579  logcn  26584  dvloglem  26585  logf1o2  26587  dvlog  26588  dvlog2lem  26589  dvlog2  26590  logtayl  26597  cxpcn  26682  cxpcnOLD  26683  cxpcn2  26684  cxpcn3  26686  resqrtcn  26687  efrlim  26907  efrlimOLD  26908  dfef2  26909  cxp2lim  26915  basellem3  27021  basellem4  27022  sqff1o  27120  dchrmhm  27180  chtppilim  27414  chto1lb  27417  chpchtlim  27418  chpo1ub  27419  dchrisumlema  27427  selberg2lem  27489  selberg3lem2  27497  pntrsumo1  27504  pnt2  27552  pnt  27553  madef  27798  onsiso  28206  n0ssold  28282  bdayn0sf1o  28296  dfnns2  28298  axcontlem2  28945  usgrexmplef  29239  griedg0ssusgr  29245  nbgrssvtx  29322  nbgrssovtx  29341  uvtxssvtx  29370  rgrusgrprc  29570  clwlkswks  29756  wwlkssswrd  29842  wwlkssswwlksn  29846  wspthsswwlkn  29898  wspthsswwlknon  29901  clwwlksclwwlkn  30013  phrel  30797  bnrel  30849  hlrel  30872  shex  31194  chsssh  31207  hhssnv  31246  choc1  31309  shunssi  31350  shsleji  31352  shsub1i  31354  shsub2i  31355  shsidmi  31366  omlsii  31385  spanuni  31526  spansni  31539  5oalem7  31642  3oalem3  31646  pjrni  31684  mayete3i  31710  hmopex  31857  cnlnssadj  32062  adjbdln  32065  adjsslnop  32069  shatomistici  32343  hatomistici  32344  xrge0tsmsd  33049  primefldchr  33274  1fldgenq  33295  zringidom  33523  esumpcvgval  34112  hashf2  34118  insiga  34171  sigapisys  34189  sigaldsys  34193  sigapildsys  34196  sxbrsigalem0  34305  dya2icobrsiga  34310  sxbrsigalem1  34319  sxbrsigalem2  34320  eulerpartlemb  34402  chtvalz  34663  logdivsqrle  34684  bnj1398  35067  bnj1498  35094  r1omfi  35137  fineqvacALT  35161  erdszelem9  35264  erdsze2lem2  35269  kur14lem9  35279  ptpconn  35298  iinllyconn  35319  cvmlift3  35393  mppsthm  35644  imagesset  36018  altxpsspw  36042  topjoin  36430  onsstopbas  36494  onsucconni  36502  onintopssconn  36505  onint1  36514  oninhaus  36515  bj-snglss  37035  bj-imdirco  37255  bj-modssabl  37345  bj-rvecssmod  37361  bj-rvecssvec  37366  bj-rvecsscmod  37368  icoreunrn  37424  difunieq  37439  poimirlem8  37688  poimirlem18  37698  poimirlem21  37701  poimirlem22  37702  poimirlem31  37711  poimirlem32  37712  heiborlem3  37873  atssbase  39409  readvrec2  42479  eldioph3b  42882  diophin  42889  diophun  42890  eldiophss  42891  isnumbasabl  43223  isnumbasgrp  43224  dfacbasgrp  43225  mon1psubm  43316  omssrncard  43657  inintabss  43695  intimass  43771  inaex  44414  nzin  44435  unipwrVD  44948  unipwr  44949  supxrre3  45448  fsumiunss  45699  rrpsscn  45712  dvnmul  46065  dvnprodlem2  46069  stoweidlem34  46156  stirlinglem13  46208  fourierdlem20  46249  fourierdlem62  46290  fourierdlem83  46311  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fouriersw  46353  qndenserrnbllem  46416  sge0iunmptlemre  46537  nn0ssge0  46546  sge0isum  46549  sge0seq  46568  sge0reuz  46569  caragendifcl  46636  carageniuncllem2  46644  hoicvrrex  46678  smfaddlem1  46885  smfaddlem2  46886  mbfpsssmf  46905  clnbgrssvtx  47955  srhmsubcALTV  48449  lvecpsslmod  48632  thincssc  49549  aacllem  49926  amgmwlem  49927  amgmlemALT  49928