Theorem ssriv 3938

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902

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 3919

This theorem is referenced by:  ssid  3957  ssv  3959  ssrab2  4030  difss  4086  ssun1  4128  inss1  4187  0ss  4350  difprsnss  4751  snsspw  4796  uniin  4883  pwuni  4896  iuniin  4954  iunpwss  5055  relopabi  5762  dmin  5851  dmrnssfld  5913  dmcoss  5914  dmcossOLD  5915  dminss  6100  imainss  6101  fvssunirn  6853  fviss  6899  opabresex2  7400  fvmptopab  7401  mapfoss  8776  fsetsspwxp  8777  mapsspm  8800  pmsspw  8801  uniixp  8845  pwfilem  9202  dffi3  9315  dfom3  9537  onwf  9720  tcrank  9774  djuss  9810  djuunxp  9811  djuun  9816  cardprclem  9869  alephsson  9988  ackbij1  10125  cardcf  10140  cfeq0  10144  dfacfin7  10287  hsmexlem6  10319  canthnum  10537  inaprc  10724  nqerf  10818  addnqf  10836  mulnqf  10837  dmrecnq  10856  reclem2pr  10936  wuncn  11058  zssre  12472  zsscn  12473  nnssz  12487  elq  12845  zssq  12851  qssre  12854  ixxssixx  13256  iooval2  13275  ioossre  13304  rge0ssre  13353  fzssz  13423  fz1ssnn  13452  fzssuz  13462  fzssp1  13464  uzdisj  13494  fz0ssnn0  13519  nn0disj  13541  fzossfz  13575  fzouzsplit  13591  fzo0ssnn0  13643  uzrdgfni  13862  seqcoll  14368  wrdexb  14429  fclim  15457  isercolllem3  15571  climcnds  15755  divcnv  15757  harmonic  15763  bitsss  16334  prmssnn  16584  maxprmfct  16617  1arith  16836  4sqlem19  16872  vdwlem12  16901  restsspw  17332  mremre  17503  mreacs  17561  isfunc  17768  homarel  17940  ledm  18493  lern  18494  chnexg  18521  smndex1basss  18810  sgrpssmgm  18838  mndsssgrp  18839  prdsgrpd  18960  prdsinvgd  18961  symgpssefmnd  19306  symgsubmefmndALT  19313  pgrpsubgsymg  19319  symgtrf  19379  odf1o2  19483  sylow3lem3  19539  sylow3lem6  19542  oppglsm  19552  efgsfo  19649  0frgp  19689  prdscmnd  19771  prdsabld  19772  dprdssv  19928  dprdres  19940  prdsrngd  20092  ringssrng  20202  prdsringd  20237  prdscrngd  20238  unitss  20292  subrngint  20473  subrgint  20508  srhmsubc  20593  subdrgint  20716  sdrgint  20717  primefld  20718  lssintcl  20895  prdslmodd  20900  cnsubmlem  21349  cnsubglem  21350  cnsubdrglem  21353  cnmsubglem  21365  xrge0subm  21378  zringunit  21401  zringlpir  21402  znf1o  21486  ocvss  21605  dsmmsubg  21678  dsmmlss  21679  lbslinds  21768  unitg  22880  cldss2  22943  indiscld  23004  iscldtop  23008  llyssnlly  23391  llyidm  23401  nllyidm  23402  toplly  23403  hauslly  23405  lly1stc  23409  dissnref  23441  txindis  23547  pthaus  23551  ptcmpfi  23726  ufinffr  23842  cnflf2  23916  flimfcls  23939  alexsubALTlem3  23962  ptcmplem1  23965  ptcmpg  23970  prdstmdd  24037  prdstgpd  24038  ust0  24133  prdsms  24444  qdensere  24682  blssioo  24708  tgioo  24709  xrtgioo  24720  xrsmopn  24726  zdis  24730  reperflem  24732  xrge0gsumle  24747  xrge0tsms  24748  icopnfhmeo  24866  bndth  24882  voliunlem2  25477  voliunlem3  25478  vitali  25539  ismbf3d  25580  itg2seq  25668  limccl  25801  limcresi  25811  dvef  25909  aasscn  26251  qssaa  26257  aannenlem2  26262  aannenlem3  26263  ulmcn  26333  mtestbdd  26339  iblulm  26341  reeff1o  26382  reefgim  26385  efifo  26481  dfrelog  26499  relogf1o  26500  logdmss  26576  logcn  26581  dvloglem  26582  logf1o2  26584  dvlog  26585  dvlog2lem  26586  dvlog2  26587  logtayl  26594  cxpcn  26679  cxpcnOLD  26680  cxpcn2  26681  cxpcn3  26683  resqrtcn  26684  efrlim  26904  efrlimOLD  26905  dfef2  26906  cxp2lim  26912  basellem3  27018  basellem4  27019  sqff1o  27117  dchrmhm  27177  chtppilim  27411  chto1lb  27414  chpchtlim  27415  chpo1ub  27416  dchrisumlema  27424  selberg2lem  27486  selberg3lem2  27494  pntrsumo1  27501  pnt2  27549  pnt  27550  madef  27795  onsiso  28203  n0ssold  28279  bdayn0sf1o  28293  dfnns2  28295  axcontlem2  28941  usgrexmplef  29235  griedg0ssusgr  29241  nbgrssvtx  29318  nbgrssovtx  29337  uvtxssvtx  29366  rgrusgrprc  29566  clwlkswks  29752  wwlkssswrd  29838  wwlkssswwlksn  29842  wspthsswwlkn  29894  wspthsswwlknon  29897  clwwlksclwwlkn  30006  phrel  30790  bnrel  30842  hlrel  30865  shex  31187  chsssh  31200  hhssnv  31239  choc1  31302  shunssi  31343  shsleji  31345  shsub1i  31347  shsub2i  31348  shsidmi  31359  omlsii  31378  spanuni  31519  spansni  31532  5oalem7  31635  3oalem3  31639  pjrni  31677  mayete3i  31703  hmopex  31850  cnlnssadj  32055  adjbdln  32058  adjsslnop  32062  shatomistici  32336  hatomistici  32337  xrge0tsmsd  33037  primefldchr  33262  1fldgenq  33283  zringidom  33511  esumpcvgval  34086  hashf2  34092  insiga  34145  sigapisys  34163  sigaldsys  34167  sigapildsys  34170  sxbrsigalem0  34279  dya2icobrsiga  34284  sxbrsigalem1  34293  sxbrsigalem2  34294  eulerpartlemb  34376  chtvalz  34637  logdivsqrle  34658  bnj1398  35041  bnj1498  35068  r1omfi  35107  fineqvacALT  35128  erdszelem9  35231  erdsze2lem2  35236  kur14lem9  35246  ptpconn  35265  iinllyconn  35286  cvmlift3  35360  mppsthm  35611  imagesset  35986  altxpsspw  36010  topjoin  36398  onsstopbas  36462  onsucconni  36470  onintopssconn  36473  onint1  36482  oninhaus  36483  bj-snglss  37003  bj-imdirco  37223  bj-modssabl  37313  bj-rvecssmod  37329  bj-rvecssvec  37334  bj-rvecsscmod  37336  icoreunrn  37392  difunieq  37407  poimirlem8  37667  poimirlem18  37677  poimirlem21  37680  poimirlem22  37681  poimirlem31  37690  poimirlem32  37691  heiborlem3  37852  atssbase  39328  readvrec2  42393  eldioph3b  42797  diophin  42804  diophun  42805  eldiophss  42806  isnumbasabl  43138  isnumbasgrp  43139  dfacbasgrp  43140  mon1psubm  43231  omssrncard  43572  inintabss  43610  intimass  43686  inaex  44329  nzin  44350  unipwrVD  44863  unipwr  44864  supxrre3  45363  fsumiunss  45614  rrpsscn  45627  dvnmul  45980  dvnprodlem2  45984  stoweidlem34  46071  stirlinglem13  46123  fourierdlem20  46164  fourierdlem62  46205  fourierdlem83  46226  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fouriersw  46268  qndenserrnbllem  46331  sge0iunmptlemre  46452  nn0ssge0  46461  sge0isum  46464  sge0seq  46483  sge0reuz  46484  caragendifcl  46551  carageniuncllem2  46559  hoicvrrex  46593  smfaddlem1  46800  smfaddlem2  46801  mbfpsssmf  46820  clnbgrssvtx  47861  srhmsubcALTV  48355  lvecpsslmod  48538  thincssc  49455  aacllem  49832  amgmwlem  49833  amgmlemALT  49834