Theorem ssriv 3937

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

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

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 3918

This theorem is referenced by:  ssid  3956  ssv  3958  ssrab2  4032  difss  4088  ssun1  4130  inss1  4189  0ss  4352  difprsnss  4755  snsspw  4800  uniin  4887  pwuni  4901  iuniin  4959  iunpwss  5062  relopabi  5771  dmin  5860  dmrnssfld  5923  dmcoss  5924  dmcossOLD  5925  dminss  6111  imainss  6112  fvssunirn  6865  fviss  6911  opabresex2  7412  fvmptopab  7413  mapfoss  8789  fsetsspwxp  8790  mapsspm  8814  pmsspw  8815  uniixp  8859  pwfilem  9218  dffi3  9334  dfom3  9556  onwf  9742  tcrank  9796  djuss  9832  djuunxp  9833  djuun  9838  cardprclem  9891  alephsson  10010  ackbij1  10147  cardcf  10162  cfeq0  10166  dfacfin7  10309  hsmexlem6  10341  canthnum  10560  inaprc  10747  nqerf  10841  addnqf  10859  mulnqf  10860  dmrecnq  10879  reclem2pr  10959  wuncn  11081  zssre  12495  zsscn  12496  nnssz  12510  elq  12863  zssq  12869  qssre  12872  ixxssixx  13275  iooval2  13294  ioossre  13323  rge0ssre  13372  fzssz  13442  fz1ssnn  13471  fzssuz  13481  fzssp1  13483  uzdisj  13513  fz0ssnn0  13538  nn0disj  13560  fzossfz  13594  fzouzsplit  13610  fzo0ssnn0  13662  uzrdgfni  13881  seqcoll  14387  wrdexb  14448  fclim  15476  isercolllem3  15590  climcnds  15774  divcnv  15776  harmonic  15782  bitsss  16353  prmssnn  16603  maxprmfct  16636  1arith  16855  4sqlem19  16891  vdwlem12  16920  restsspw  17351  mremre  17523  mreacs  17581  isfunc  17788  homarel  17960  ledm  18513  lern  18514  chnexg  18541  smndex1basss  18830  sgrpssmgm  18858  mndsssgrp  18859  prdsgrpd  18980  prdsinvgd  18981  symgpssefmnd  19325  symgsubmefmndALT  19332  pgrpsubgsymg  19338  symgtrf  19398  odf1o2  19502  sylow3lem3  19558  sylow3lem6  19561  oppglsm  19571  efgsfo  19668  0frgp  19708  prdscmnd  19790  prdsabld  19791  dprdssv  19947  dprdres  19959  prdsrngd  20111  ringssrng  20221  prdsringd  20256  prdscrngd  20257  unitss  20312  subrngint  20493  subrgint  20528  srhmsubc  20613  subdrgint  20736  sdrgint  20737  primefld  20738  lssintcl  20915  prdslmodd  20920  cnsubmlem  21369  cnsubglem  21370  cnsubdrglem  21373  cnmsubglem  21385  xrge0subm  21398  zringunit  21421  zringlpir  21422  znf1o  21506  ocvss  21625  dsmmsubg  21698  dsmmlss  21699  lbslinds  21788  unitg  22911  cldss2  22974  indiscld  23035  iscldtop  23039  llyssnlly  23422  llyidm  23432  nllyidm  23433  toplly  23434  hauslly  23436  lly1stc  23440  dissnref  23472  txindis  23578  pthaus  23582  ptcmpfi  23757  ufinffr  23873  cnflf2  23947  flimfcls  23970  alexsubALTlem3  23993  ptcmplem1  23996  ptcmpg  24001  prdstmdd  24068  prdstgpd  24069  ust0  24164  prdsms  24475  qdensere  24713  blssioo  24739  tgioo  24740  xrtgioo  24751  xrsmopn  24757  zdis  24761  reperflem  24763  xrge0gsumle  24778  xrge0tsms  24779  icopnfhmeo  24897  bndth  24913  voliunlem2  25508  voliunlem3  25509  vitali  25570  ismbf3d  25611  itg2seq  25699  limccl  25832  limcresi  25842  dvef  25940  aasscn  26282  qssaa  26288  aannenlem2  26293  aannenlem3  26294  ulmcn  26364  mtestbdd  26370  iblulm  26372  reeff1o  26413  reefgim  26416  efifo  26512  dfrelog  26530  relogf1o  26531  logdmss  26607  logcn  26612  dvloglem  26613  logf1o2  26615  dvlog  26616  dvlog2lem  26617  dvlog2  26618  logtayl  26625  cxpcn  26710  cxpcnOLD  26711  cxpcn2  26712  cxpcn3  26714  resqrtcn  26715  efrlim  26935  efrlimOLD  26936  dfef2  26937  cxp2lim  26943  basellem3  27049  basellem4  27050  sqff1o  27148  dchrmhm  27208  chtppilim  27442  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  dchrisumlema  27455  selberg2lem  27517  selberg3lem2  27525  pntrsumo1  27532  pnt2  27580  pnt  27581  madef  27832  oniso  28267  bdayn0sf1o  28366  dfnns2  28368  axcontlem2  29038  usgrexmplef  29332  griedg0ssusgr  29338  nbgrssvtx  29415  nbgrssovtx  29434  uvtxssvtx  29463  rgrusgrprc  29663  clwlkswks  29849  wwlkssswrd  29935  wwlkssswwlksn  29939  wspthsswwlkn  29991  wspthsswwlknon  29994  clwwlksclwwlkn  30106  phrel  30890  bnrel  30942  hlrel  30965  shex  31287  chsssh  31300  hhssnv  31339  choc1  31402  shunssi  31443  shsleji  31445  shsub1i  31447  shsub2i  31448  shsidmi  31459  omlsii  31478  spanuni  31619  spansni  31632  5oalem7  31735  3oalem3  31739  pjrni  31777  mayete3i  31803  hmopex  31950  cnlnssadj  32155  adjbdln  32158  adjsslnop  32162  shatomistici  32436  hatomistici  32437  xrge0tsmsd  33155  primefldchr  33383  1fldgenq  33404  zringidom  33632  esumpcvgval  34235  hashf2  34241  insiga  34294  sigapisys  34312  sigaldsys  34316  sigapildsys  34319  sxbrsigalem0  34428  dya2icobrsiga  34433  sxbrsigalem1  34442  sxbrsigalem2  34443  eulerpartlemb  34525  chtvalz  34786  logdivsqrle  34807  bnj1398  35190  bnj1498  35217  r1omfi  35261  fineqvacALT  35273  erdszelem9  35393  erdsze2lem2  35398  kur14lem9  35408  ptpconn  35427  iinllyconn  35448  cvmlift3  35522  mppsthm  35773  imagesset  36147  altxpsspw  36171  topjoin  36559  onsstopbas  36623  onsucconni  36631  onintopssconn  36634  onint1  36643  oninhaus  36644  bj-snglss  37171  bj-imdirco  37391  bj-modssabl  37481  bj-rvecssmod  37497  bj-rvecssvec  37502  bj-rvecsscmod  37504  icoreunrn  37560  difunieq  37575  poimirlem8  37825  poimirlem18  37835  poimirlem21  37838  poimirlem22  37839  poimirlem31  37848  poimirlem32  37849  heiborlem3  38010  atssbase  39546  readvrec2  42612  eldioph3b  43003  diophin  43010  diophun  43011  eldiophss  43012  isnumbasabl  43344  isnumbasgrp  43345  dfacbasgrp  43346  mon1psubm  43437  omssrncard  43777  inintabss  43815  intimass  43891  inaex  44534  nzin  44555  unipwrVD  45068  unipwr  45069  supxrre3  45566  fsumiunss  45817  rrpsscn  45830  dvnmul  46183  dvnprodlem2  46187  stoweidlem34  46274  stirlinglem13  46326  fourierdlem20  46367  fourierdlem62  46408  fourierdlem83  46429  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fouriersw  46471  qndenserrnbllem  46534  sge0iunmptlemre  46655  nn0ssge0  46664  sge0isum  46667  sge0seq  46686  sge0reuz  46687  caragendifcl  46754  carageniuncllem2  46762  hoicvrrex  46796  smfaddlem1  47003  smfaddlem2  47004  mbfpsssmf  47023  clnbgrssvtx  48073  srhmsubcALTV  48567  lvecpsslmod  48749  thincssc  49665  aacllem  50042  amgmwlem  50043  amgmlemALT  50044