Theorem ssriv 3941

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905

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

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

This theorem is referenced by:  ssid  3960  ssv  3962  ssrab2  4033  difss  4089  ssun1  4131  inss1  4190  0ss  4353  difprsnss  4753  snsspw  4798  uniin  4885  pwuni  4898  iuniin  4957  iunpwss  5059  relopabi  5769  dmin  5858  dmrnssfld  5919  dmcoss  5920  dmcossOLD  5921  dminss  6106  imainss  6107  fvssunirn  6857  fviss  6904  opabresex2  7407  fvmptopab  7408  mapfoss  8786  fsetsspwxp  8787  mapsspm  8810  pmsspw  8811  uniixp  8855  pwfilem  9225  dffi3  9340  dfom3  9562  onwf  9745  tcrank  9799  djuss  9835  djuunxp  9836  djuun  9841  cardprclem  9894  alephsson  10013  ackbij1  10150  cardcf  10165  cfeq0  10169  dfacfin7  10312  hsmexlem6  10344  canthnum  10562  inaprc  10749  nqerf  10843  addnqf  10861  mulnqf  10862  dmrecnq  10881  reclem2pr  10961  wuncn  11083  zssre  12496  zsscn  12497  nnssz  12511  elq  12869  zssq  12875  qssre  12878  ixxssixx  13280  iooval2  13299  ioossre  13328  rge0ssre  13377  fzssz  13447  fz1ssnn  13476  fzssuz  13486  fzssp1  13488  uzdisj  13518  fz0ssnn0  13543  nn0disj  13565  fzossfz  13599  fzouzsplit  13615  fzo0ssnn0  13667  uzrdgfni  13883  seqcoll  14389  wrdexb  14450  fclim  15478  isercolllem3  15592  climcnds  15776  divcnv  15778  harmonic  15784  bitsss  16355  prmssnn  16605  maxprmfct  16638  1arith  16857  4sqlem19  16893  vdwlem12  16922  restsspw  17353  mremre  17524  mreacs  17582  isfunc  17789  homarel  17961  ledm  18514  lern  18515  smndex1basss  18797  sgrpssmgm  18825  mndsssgrp  18826  prdsgrpd  18947  prdsinvgd  18948  symgpssefmnd  19293  symgsubmefmndALT  19300  pgrpsubgsymg  19306  symgtrf  19366  odf1o2  19470  sylow3lem3  19526  sylow3lem6  19529  oppglsm  19539  efgsfo  19636  0frgp  19676  prdscmnd  19758  prdsabld  19759  dprdssv  19915  dprdres  19927  prdsrngd  20079  ringssrng  20189  prdsringd  20224  prdscrngd  20225  unitss  20279  subrngint  20463  subrgint  20498  srhmsubc  20583  subdrgint  20706  sdrgint  20707  primefld  20708  lssintcl  20885  prdslmodd  20890  cnsubmlem  21339  cnsubglem  21340  cnsubdrglem  21343  cnmsubglem  21355  xrge0subm  21368  zringunit  21391  zringlpir  21392  znf1o  21476  ocvss  21595  dsmmsubg  21668  dsmmlss  21669  lbslinds  21758  unitg  22870  cldss2  22933  indiscld  22994  iscldtop  22998  llyssnlly  23381  llyidm  23391  nllyidm  23392  toplly  23393  hauslly  23395  lly1stc  23399  dissnref  23431  txindis  23537  pthaus  23541  ptcmpfi  23716  ufinffr  23832  cnflf2  23906  flimfcls  23929  alexsubALTlem3  23952  ptcmplem1  23955  ptcmpg  23960  prdstmdd  24027  prdstgpd  24028  ust0  24123  prdsms  24435  qdensere  24673  blssioo  24699  tgioo  24700  xrtgioo  24711  xrsmopn  24717  zdis  24721  reperflem  24723  xrge0gsumle  24738  xrge0tsms  24739  icopnfhmeo  24857  bndth  24873  voliunlem2  25468  voliunlem3  25469  vitali  25530  ismbf3d  25571  itg2seq  25659  limccl  25792  limcresi  25802  dvef  25900  aasscn  26242  qssaa  26248  aannenlem2  26253  aannenlem3  26254  ulmcn  26324  mtestbdd  26330  iblulm  26332  reeff1o  26373  reefgim  26376  efifo  26472  dfrelog  26490  relogf1o  26491  logdmss  26567  logcn  26572  dvloglem  26573  logf1o2  26575  dvlog  26576  dvlog2lem  26577  dvlog2  26578  logtayl  26585  cxpcn  26670  cxpcnOLD  26671  cxpcn2  26672  cxpcn3  26674  resqrtcn  26675  efrlim  26895  efrlimOLD  26896  dfef2  26897  cxp2lim  26903  basellem3  27009  basellem4  27010  sqff1o  27108  dchrmhm  27168  chtppilim  27402  chto1lb  27405  chpchtlim  27406  chpo1ub  27407  dchrisumlema  27415  selberg2lem  27477  selberg3lem2  27485  pntrsumo1  27492  pnt2  27540  pnt  27541  madef  27784  onsiso  28192  n0ssold  28268  bdayn0sf1o  28282  dfnns2  28284  axcontlem2  28928  usgrexmplef  29222  griedg0ssusgr  29228  nbgrssvtx  29305  nbgrssovtx  29324  uvtxssvtx  29353  rgrusgrprc  29553  clwlkswks  29739  wwlkssswrd  29825  wwlkssswwlksn  29829  wspthsswwlkn  29881  wspthsswwlknon  29884  clwwlksclwwlkn  29993  phrel  30777  bnrel  30829  hlrel  30852  shex  31174  chsssh  31187  hhssnv  31226  choc1  31289  shunssi  31330  shsleji  31332  shsub1i  31334  shsub2i  31335  shsidmi  31346  omlsii  31365  spanuni  31506  spansni  31519  5oalem7  31622  3oalem3  31626  pjrni  31664  mayete3i  31690  hmopex  31837  cnlnssadj  32042  adjbdln  32045  adjsslnop  32049  shatomistici  32323  hatomistici  32324  xrge0tsmsd  33028  primefldchr  33250  1fldgenq  33271  zringidom  33498  esumpcvgval  34044  hashf2  34050  insiga  34103  sigapisys  34121  sigaldsys  34125  sigapildsys  34128  sxbrsigalem0  34238  dya2icobrsiga  34243  sxbrsigalem1  34252  sxbrsigalem2  34253  eulerpartlemb  34335  chtvalz  34596  logdivsqrle  34617  bnj1398  35000  bnj1498  35027  fineqvacALT  35072  erdszelem9  35171  erdsze2lem2  35176  kur14lem9  35186  ptpconn  35205  iinllyconn  35226  cvmlift3  35300  mppsthm  35551  imagesset  35926  altxpsspw  35950  topjoin  36338  onsstopbas  36402  onsucconni  36410  onintopssconn  36413  onint1  36422  oninhaus  36423  bj-snglss  36943  bj-imdirco  37163  bj-modssabl  37253  bj-rvecssmod  37269  bj-rvecssvec  37274  bj-rvecsscmod  37276  icoreunrn  37332  difunieq  37347  poimirlem8  37607  poimirlem18  37617  poimirlem21  37620  poimirlem22  37621  poimirlem31  37630  poimirlem32  37631  heiborlem3  37792  atssbase  39268  readvrec2  42334  eldioph3b  42738  diophin  42745  diophun  42746  eldiophss  42747  isnumbasabl  43079  isnumbasgrp  43080  dfacbasgrp  43081  mon1psubm  43172  omssrncard  43513  inintabss  43551  intimass  43627  inaex  44270  nzin  44291  unipwrVD  44805  unipwr  44806  supxrre3  45305  fsumiunss  45557  rrpsscn  45570  dvnmul  45925  dvnprodlem2  45929  stoweidlem34  46016  stirlinglem13  46068  fourierdlem20  46109  fourierdlem62  46150  fourierdlem83  46171  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fouriersw  46213  qndenserrnbllem  46276  sge0iunmptlemre  46397  nn0ssge0  46406  sge0isum  46409  sge0seq  46428  sge0reuz  46429  caragendifcl  46496  carageniuncllem2  46504  hoicvrrex  46538  smfaddlem1  46745  smfaddlem2  46746  mbfpsssmf  46765  upwordsseti  46867  clnbgrssvtx  47816  srhmsubcALTV  48310  lvecpsslmod  48493  thincssc  49410  aacllem  49787  amgmwlem  49788  amgmlemALT  49789