Theorem ssriv 3893

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

Syntax hints:   → wi 4   ∈ wcel 2081   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874

This theorem is referenced by:  ssid  3910  ssv  3912  difss  4029  ssun1  4069  inss1  4125  0ss  4270  difprsnss  4639  snsspw  4682  uniin  4765  pwuni  4781  iuniin  4836  iunpwss  4928  pwunss  5343  relopabi  5580  dmin  5666  dmrnssfld  5722  dmcoss  5723  dminss  5886  imainss  5887  fviss  6608  mapsspm  8290  pmsspw  8291  uniixp  8333  pwfilem  8664  dffi3  8741  dfom3  8956  onwf  9105  tcrank  9159  djuss  9195  djuunxp  9196  djuun  9201  cardprclem  9254  alephsson  9372  ackbij1  9506  cardcf  9520  cfeq0  9524  dfacfin7  9667  hsmexlem6  9699  canthnum  9917  inaprc  10104  nqerf  10198  addnqf  10216  mulnqf  10217  dmrecnq  10236  reclem2pr  10316  wuncn  10438  zssre  11836  zsscn  11837  nnssz  11850  nnsszOLD  11851  elq  12199  zssq  12205  qssre  12208  ixxssixx  12602  iooval2  12621  ioossre  12648  rge0ssre  12694  fzssz  12759  fz1ssnn  12788  fzssuz  12798  fzssp1  12800  uzdisj  12830  fz0ssnn0  12852  nn0disj  12873  fzossfz  12906  fzouzsplit  12922  fzo0ssnn0  12968  uzrdgfni  13176  seqcoll  13670  wrdexgOLD  13718  wrdexb  13719  fclim  14744  isercolllem3  14857  climcnds  15039  divcnv  15041  harmonic  15047  bitsss  15608  prmssnn  15849  maxprmfct  15882  1arith  16092  4sqlem19  16128  vdwlem12  16157  restsspw  16534  mremre  16704  mreacs  16758  isfunc  16963  homarel  17125  ledm  17663  lern  17664  sgrpssmgm  17859  mndsssgrp  17860  prdsgrpd  17966  prdsinvgd  17967  symgtrf  18328  odf1o2  18428  sylow3lem3  18484  sylow3lem6  18487  oppglsm  18497  efgsfo  18592  0frgp  18632  prdscmnd  18704  prdsabld  18705  dprdssv  18855  dprdres  18867  prdsringd  19052  prdscrngd  19053  unitss  19100  subrgint  19247  subdrgint  19272  sdrgint  19273  primefld  19274  lssintcl  19426  prdslmodd  19431  xrge0subm  20268  cnsubmlem  20275  cnsubglem  20276  cnsubdrglem  20278  cnmsubglem  20290  zringunit  20317  zringlpir  20318  znf1o  20380  zntoslem  20385  ocvss  20496  dsmmsubg  20569  dsmmlss  20570  lbslinds  20659  unitg  21259  cldss2  21322  indiscld  21383  iscldtop  21387  llyssnlly  21770  llyidm  21780  nllyidm  21781  toplly  21782  hauslly  21784  lly1stc  21788  dissnref  21820  txindis  21926  pthaus  21930  ptcmpfi  22105  ufinffr  22221  cnflf2  22295  flimfcls  22318  alexsubALTlem3  22341  ptcmplem1  22344  ptcmpg  22349  prdstmdd  22415  prdstgpd  22416  ust0  22511  prdsms  22824  qdensere  23061  blssioo  23086  tgioo  23087  xrtgioo  23097  xrsmopn  23103  zdis  23107  reperflem  23109  xrge0gsumle  23124  xrge0tsms  23125  icopnfhmeo  23230  bndth  23245  voliunlem2  23835  voliunlem3  23836  vitali  23897  ismbf3d  23938  itg2seq  24026  limccl  24156  limcresi  24166  dvef  24260  aasscn  24590  qssaa  24596  aannenlem2  24601  aannenlem3  24602  ulmcn  24670  mtestbdd  24676  iblulm  24678  reeff1o  24718  reefgim  24721  efifo  24812  dfrelog  24830  relogf1o  24831  logdmss  24906  logcn  24911  dvloglem  24912  logf1o2  24914  dvlog  24915  dvlog2lem  24916  dvlog2  24917  logtayl  24924  cxpcn  25007  cxpcn2  25008  cxpcn3  25010  resqrtcn  25011  efrlim  25229  dfef2  25230  cxp2lim  25236  basellem3  25342  basellem4  25343  sqff1o  25441  dchrmhm  25499  chtppilim  25733  chto1lb  25736  chpchtlim  25737  chpo1ub  25738  dchrisumlema  25746  selberg2lem  25808  selberg3lem2  25816  pntrsumo1  25823  pnt2  25871  pnt  25872  axcontlem2  26434  usgrexmplef  26724  griedg0ssusgr  26730  nbgrssvtx  26807  nbgrssovtx  26826  uvtxssvtx  26855  rgrusgrprc  27054  clwlkswks  27244  wwlkssswrd  27327  wwlkssswwlksn  27331  wspthsswwlkn  27384  wspthsswwlknon  27387  clwwlksclwwlkn  27496  phrel  28283  bnrel  28335  hlrel  28358  shex  28680  chsssh  28693  hhssnv  28732  choc1  28795  shunssi  28836  shsleji  28838  shsub1i  28840  shsub2i  28841  shsidmi  28852  omlsii  28871  spanuni  29012  spansni  29025  5oalem7  29128  3oalem3  29132  pjrni  29170  mayete3i  29196  hmopex  29343  cnlnssadj  29548  adjbdln  29551  adjsslnop  29555  shatomistici  29829  hatomistici  29830  xrge0tsmsd  30503  primefldchr  30521  esumpcvgval  30954  hashf2  30960  insiga  31013  sigapisys  31031  sigaldsys  31035  sigapildsys  31038  sxbrsigalem0  31146  dya2icobrsiga  31151  sxbrsigalem1  31160  sxbrsigalem2  31161  eulerpartlemb  31243  chtvalz  31517  logdivsqrle  31538  bnj1398  31920  bnj1498  31947  erdszelem9  32054  erdsze2lem2  32059  kur14lem9  32069  ptpconn  32088  iinllyconn  32109  cvmlift3  32183  mppsthm  32434  imagesset  33023  altxpsspw  33047  topjoin  33322  onsstopbas  33386  onsucconni  33394  onintopssconn  33397  onint1  33406  oninhaus  33407  bj-snglss  33887  bj-modssabl  34114  icoreunrn  34171  difunieq  34186  poimirlem8  34431  poimirlem18  34441  poimirlem21  34444  poimirlem22  34445  poimirlem31  34454  poimirlem32  34455  heiborlem3  34623  atssbase  35957  eldioph3b  38847  diophin  38854  diophun  38855  eldiophss  38856  isnumbasabl  39191  isnumbasgrp  39192  dfacbasgrp  39193  mon1psubm  39291  inintabss  39423  intimass  39484  inaex  40130  nzin  40188  unipwrVD  40705  unipwr  40706  supxrre3  41134  fsumiunss  41398  rrpsscn  41411  dvnmul  41769  dvnprodlem2  41773  stoweidlem34  41861  stirlinglem13  41913  fourierdlem20  41954  fourierdlem62  41995  fourierdlem83  42016  fourierdlem101  42034  fourierdlem103  42036  fourierdlem104  42037  fourierdlem111  42044  fouriersw  42058  qndenserrnbllem  42121  sge0iunmptlemre  42239  nn0ssge0  42248  sge0isum  42251  sge0seq  42270  sge0reuz  42271  caragendifcl  42338  carageniuncllem2  42346  hoicvrrex  42380  smfaddlem1  42581  smfaddlem2  42582  mbfpsssmf  42601  ringssrng  43629  srhmsubc  43825  srhmsubcALTV  43843  lvecpsslmod  44042  aacllem  44382  amgmwlem  44383  amgmlemALT  44384