Theorem ssriv 3940

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904

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

This theorem depends on definitions:  df-bi 209  df-ss 3921

This theorem is referenced by:  ssid  3958  ssv  3960  ssrab2  4033  difss  4089  ssun1  4130  inss1  4188  0ss  4353  difprsnss  4758  snsspw  4801  uniinOLD  4889  pwuni  4903  iuniin  4961  iunpwss  5063  relopabi  5793  dmin  5885  dmrnssfld  5948  dmcoss  5949  dmcossOLD  5950  dminss  6135  imainss  6136  fvssunirn  6894  fviss  6940  opabresex2  7446  fvmptopab  7447  mapfoss  8829  fsetsspwxp  8830  mapsspm  8854  pmsspw  8855  uniixp  8899  pwfilem  9258  dffi3  9374  dfom3  9599  onwf  9785  tcrank  9839  djuss  9875  djuunxp  9876  djuun  9881  cardprclem  9934  alephsson  10053  ackbij1  10190  cardcf  10205  cfeq0  10210  dfacfin7  10353  hsmexlem6  10385  canthnum  10604  inaprc  10791  nqerf  10885  addnqf  10903  mulnqf  10904  dmrecnq  10923  reclem2pr  11003  wuncn  11125  zssre  12572  zsscn  12573  nnssz  12587  elq  12948  zssq  12954  qssre  12957  ixxssixx  13360  iooval2  13379  ioossre  13408  rge0ssre  13457  fzssz  13528  fz1ssnn  13557  fzssuz  13567  fzssp1  13569  uzdisj  13599  fz0ssnn0  13624  nn0disj  13646  fzossfz  13681  fzouzsplit  13697  fzo0ssnn0  13749  uzrdgfni  13968  seqcoll  14474  wrdexb  14535  fclim  15563  isercolllem3  15677  climcnds  15864  divcnv  15866  harmonic  15872  bitsss  16443  prmssnn  16693  prmssuz2  16714  maxprmfct  16727  1arith  16946  4sqlem19  16982  vdwlem12  17011  restsspw  17443  mremre  17615  mreacs  17673  isfunc  17880  homarel  18052  ledm  18605  lern  18606  chnexg  18633  smndex1basss  18925  sgrpssmgm  18953  mndsssgrp  18954  prdsgrpd  19075  prdsinvgd  19076  symgpssefmnd  19419  symgsubmefmndALT  19426  pgrpsubgsymg  19432  symgtrf  19492  odf1o2  19596  sylow3lem3  19652  sylow3lem6  19655  oppglsm  19665  efgsfo  19762  0frgp  19802  prdscmnd  19884  prdsabld  19885  dprdssv  20041  dprdres  20053  prdsrngd  20205  ringssrng  20315  prdsringd  20348  prdscrngd  20349  unitss  20404  subrngint  20589  subrgint  20624  srhmsubc  20709  subdrgint  20832  sdrgint  20833  primefld  20834  lssintcl  21011  prdslmodd  21016  cnsubmlem  21447  cnsubglem  21448  cnsubdrglem  21450  cnmsubglem  21462  xrge0subm  21475  zringunit  21498  zringlpir  21499  znf1o  21583  ocvss  21702  dsmmsubg  21775  dsmmlss  21776  lbslinds  21865  unitg  23007  cldss2  23070  indiscld  23131  iscldtop  23135  llyssnlly  23518  llyidm  23528  nllyidm  23529  toplly  23530  hauslly  23532  lly1stc  23536  dissnref  23568  txindis  23674  pthaus  23678  ptcmpfi  23853  ufinffr  23969  cnflf2  24043  flimfcls  24066  alexsubALTlem3  24089  ptcmplem1  24092  ptcmpg  24097  prdstmdd  24164  prdstgpd  24165  ust0  24260  prdsms  24571  qdensere  24809  blssioo  24835  tgioo  24836  xrtgioo  24847  xrsmopn  24853  zdis  24857  reperflem  24859  xrge0gsumle  24874  xrge0tsms  24875  icopnfhmeo  24985  bndth  25000  voliunlem2  25593  voliunlem3  25594  vitali  25655  ismbf3d  25696  itg2seq  25784  limccl  25917  limcresi  25927  dvef  26022  aasscn  26359  qssaa  26365  aannenlem2  26370  aannenlem3  26371  ulmcn  26439  mtestbdd  26445  iblulm  26447  reeff1o  26487  reefgim  26490  efifo  26589  dfrelog  26607  relogf1o  26608  logdmss  26684  logcn  26689  dvloglem  26690  logf1o2  26692  dvlog  26693  dvlog2lem  26694  dvlog2  26695  logtayl  26702  cxpcn  26787  cxpcn2  26788  cxpcn3  26790  resqrtcn  26791  efrlim  27011  dfef2  27012  cxp2lim  27018  basellem3  27124  basellem4  27125  sqff1o  27223  dchrmhm  27282  chtppilim  27516  chto1lb  27519  chpchtlim  27520  chpo1ub  27521  dchrisumlema  27529  selberg2lem  27591  selberg3lem2  27599  pntrsumo1  27606  pnt2  27654  pnt  27655  madef  27906  oniso  28341  bdayn0sf1o  28440  dfnns2  28442  axcontlem2  29112  usgrexmplef  29406  griedg0ssusgr  29412  nbgrssvtx  29489  nbgrssovtx  29508  uvtxssvtx  29537  rgrusgrprc  29736  clwlkswks  29922  wwlkssswrd  30008  wwlkssswwlksn  30012  wspthsswwlkn  30064  wspthsswwlknon  30067  clwwlksclwwlkn  30179  phrel  30964  bnrel  31016  hlrel  31039  shex  31361  chsssh  31374  hhssnv  31413  choc1  31476  shunssi  31517  shsleji  31519  shsub1i  31521  shsub2i  31522  shsidmi  31533  omlsii  31552  spanuni  31693  spansni  31706  5oalem7  31809  3oalem3  31813  pjrni  31851  mayete3i  31877  hmopex  32024  cnlnssadj  32229  adjbdln  32232  adjsslnop  32236  shatomistici  32510  hatomistici  32511  xrge0tsmsd  33214  primefldchr  33449  1fldgenq  33470  zringidom  33708  esumpcvgval  34336  hashf2  34342  insiga  34395  sigapisys  34413  sigaldsys  34417  sigapildsys  34420  sxbrsigalem0  34529  dya2icobrsiga  34534  sxbrsigalem1  34543  sxbrsigalem2  34544  eulerpartlemb  34626  chtvalz  34887  logdivsqrle  34908  bnj1398  35293  bnj1498  35320  r1omfi  35365  fineqvacALT  35377  erdszelem9  35513  erdsze2lem2  35518  kur14lem9  35528  ptpconn  35547  iinllyconn  35568  cvmlift3  35642  mppsthm  35893  imagesset  36267  altxpsspw  36291  topjoin  36689  onsstopbas  36753  onsucconni  36761  onintopssconn  36764  onint1  36773  oninhaus  36774  ttcid  36816  dfttc4lem2  36853  dfttc4  36854  bj-snglss  37419  bj-imdirco  37646  bj-modssabl  37736  bj-rvecssmod  37752  bj-rvecssvec  37757  bj-rvecsscmod  37759  icoreunrn  37817  difunieq  37832  poimirlem8  38091  poimirlem18  38101  poimirlem21  38104  poimirlem22  38105  poimirlem31  38114  poimirlem32  38115  heiborlem3  38276  disjsssrels  39399  atssbase  39878  readvrec2  42934  eldioph3b  43310  diophin  43317  diophun  43318  eldiophss  43319  isnumbasabl  43647  isnumbasgrp  43648  dfacbasgrp  43649  mon1psubm  43740  omssrncard  44080  inintabss  44118  intimass  44194  inaex  44837  nzin  44858  unipwrVD  45371  unipwr  45372  supxrre3  45865  fsumiunss  46115  rrpsscn  46128  dvnmul  46481  dvnprodlem2  46485  stoweidlem34  46572  stirlinglem13  46624  fourierdlem20  46665  fourierdlem62  46706  fourierdlem83  46727  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fouriersw  46769  qndenserrnbllem  46832  sge0iunmptlemre  46953  nn0ssge0  46962  sge0isum  46965  sge0seq  46984  sge0reuz  46985  caragendifcl  47052  carageniuncllem2  47060  hoicvrrex  47094  smfaddlem1  47301  smfaddlem2  47302  mbfpsssmf  47321  clnbgrssvtx  48417  srhmsubcALTV  48911  lvecpsslmod  49093  thincssc  50009  aacllem  50386  amgmwlem  50387  amgmlemALT  50388