Theorem ssriv 3926

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  ssid  3944  ssv  3946  ssrab2  4014  difss  4067  ssun1  4107  inss1  4163  0ss  4331  difprsnss  4733  snsspw  4776  uniin  4866  pwuni  4879  iuniin  4937  iunpwss  5037  pwunssOLD  5485  relopabi  5734  dmin  5823  dmrnssfld  5882  dmcoss  5883  dminss  6061  imainss  6062  fviss  6854  opabresex2  7336  fvmptopab  7338  mapfoss  8649  fsetsspwxp  8650  mapsspm  8673  pmsspw  8674  uniixp  8718  pwfilem  8969  pwfilemOLD  9122  dffi3  9199  dfom3  9414  onwf  9597  tcrank  9651  djuss  9687  djuunxp  9688  djuun  9693  cardprclem  9746  alephsson  9865  ackbij1  10003  cardcf  10017  cfeq0  10021  dfacfin7  10164  hsmexlem6  10196  canthnum  10414  inaprc  10601  nqerf  10695  addnqf  10713  mulnqf  10714  dmrecnq  10733  reclem2pr  10813  wuncn  10935  zssre  12335  zsscn  12336  nnssz  12349  elq  12699  zssq  12705  qssre  12708  ixxssixx  13102  iooval2  13121  ioossre  13149  rge0ssre  13197  fzssz  13267  fz1ssnn  13296  fzssuz  13306  fzssp1  13308  uzdisj  13338  fz0ssnn0  13360  nn0disj  13381  fzossfz  13415  fzouzsplit  13431  fzo0ssnn0  13477  uzrdgfni  13687  seqcoll  14187  wrdexb  14237  fclim  15271  isercolllem3  15387  climcnds  15572  divcnv  15574  harmonic  15580  bitsss  16142  prmssnn  16390  maxprmfct  16423  1arith  16637  4sqlem19  16673  vdwlem12  16702  restsspw  17151  mremre  17322  mreacs  17376  isfunc  17588  homarel  17760  ledm  18317  lern  18318  smndex1basss  18553  sgrpssmgm  18581  mndsssgrp  18582  prdsgrpd  18694  prdsinvgd  18695  symgpssefmnd  19012  symgsubmefmndALT  19020  pgrpsubgsymg  19026  symgtrf  19086  odf1o2  19187  sylow3lem3  19243  sylow3lem6  19246  oppglsm  19256  efgsfo  19354  0frgp  19394  prdscmnd  19471  prdsabld  19472  dprdssv  19628  dprdres  19640  prdsringd  19860  prdscrngd  19861  unitss  19911  subrgint  20055  subdrgint  20080  sdrgint  20081  primefld  20082  lssintcl  20235  prdslmodd  20240  xrge0subm  20648  cnsubmlem  20655  cnsubglem  20656  cnsubdrglem  20658  cnmsubglem  20670  zringunit  20697  zringlpir  20698  znf1o  20768  ocvss  20884  dsmmsubg  20959  dsmmlss  20960  lbslinds  21049  unitg  22126  cldss2  22190  indiscld  22251  iscldtop  22255  llyssnlly  22638  llyidm  22648  nllyidm  22649  toplly  22650  hauslly  22652  lly1stc  22656  dissnref  22688  txindis  22794  pthaus  22798  ptcmpfi  22973  ufinffr  23089  cnflf2  23163  flimfcls  23186  alexsubALTlem3  23209  ptcmplem1  23212  ptcmpg  23217  prdstmdd  23284  prdstgpd  23285  ust0  23380  prdsms  23696  qdensere  23942  blssioo  23967  tgioo  23968  xrtgioo  23978  xrsmopn  23984  zdis  23988  reperflem  23990  xrge0gsumle  24005  xrge0tsms  24006  icopnfhmeo  24115  bndth  24130  voliunlem2  24724  voliunlem3  24725  vitali  24786  ismbf3d  24827  itg2seq  24916  limccl  25048  limcresi  25058  dvef  25153  aasscn  25487  qssaa  25493  aannenlem2  25498  aannenlem3  25499  ulmcn  25567  mtestbdd  25573  iblulm  25575  reeff1o  25615  reefgim  25618  efifo  25712  dfrelog  25730  relogf1o  25731  logdmss  25806  logcn  25811  dvloglem  25812  logf1o2  25814  dvlog  25815  dvlog2lem  25816  dvlog2  25817  logtayl  25824  cxpcn  25907  cxpcn2  25908  cxpcn3  25910  resqrtcn  25911  efrlim  26128  dfef2  26129  cxp2lim  26135  basellem3  26241  basellem4  26242  sqff1o  26340  dchrmhm  26398  chtppilim  26632  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  dchrisumlema  26645  selberg2lem  26707  selberg3lem2  26715  pntrsumo1  26722  pnt2  26770  pnt  26771  axcontlem2  27342  usgrexmplef  27635  griedg0ssusgr  27641  nbgrssvtx  27718  nbgrssovtx  27737  uvtxssvtx  27766  rgrusgrprc  27965  clwlkswks  28153  wwlkssswrd  28236  wwlkssswwlksn  28240  wspthsswwlkn  28292  wspthsswwlknon  28295  clwwlksclwwlkn  28404  phrel  29186  bnrel  29238  hlrel  29261  shex  29583  chsssh  29596  hhssnv  29635  choc1  29698  shunssi  29739  shsleji  29741  shsub1i  29743  shsub2i  29744  shsidmi  29755  omlsii  29774  spanuni  29915  spansni  29928  5oalem7  30031  3oalem3  30035  pjrni  30073  mayete3i  30099  hmopex  30246  cnlnssadj  30451  adjbdln  30454  adjsslnop  30458  shatomistici  30732  hatomistici  30733  xrge0tsmsd  31326  primefldchr  31502  esumpcvgval  32055  hashf2  32061  insiga  32114  sigapisys  32132  sigaldsys  32136  sigapildsys  32139  sxbrsigalem0  32247  dya2icobrsiga  32252  sxbrsigalem1  32261  sxbrsigalem2  32262  eulerpartlemb  32344  chtvalz  32618  logdivsqrle  32639  bnj1398  33023  bnj1498  33050  fineqvacALT  33076  erdszelem9  33170  erdsze2lem2  33175  kur14lem9  33185  ptpconn  33204  iinllyconn  33225  cvmlift3  33299  mppsthm  33550  madef  34049  imagesset  34264  altxpsspw  34288  topjoin  34563  onsstopbas  34627  onsucconni  34635  onintopssconn  34638  onint1  34647  oninhaus  34648  bj-snglss  35169  bj-imdirco  35370  bj-modssabl  35460  bj-rvecssmod  35476  bj-rvecssvec  35481  bj-rvecsscmod  35483  icoreunrn  35539  difunieq  35554  poimirlem8  35794  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem31  35817  poimirlem32  35818  heiborlem3  35980  atssbase  37311  eldioph3b  40594  diophin  40601  diophun  40602  eldiophss  40603  isnumbasabl  40938  isnumbasgrp  40939  dfacbasgrp  40940  mon1psubm  41038  omssrncard  41154  inintabss  41193  intimass  41269  inaex  41922  nzin  41943  unipwrVD  42459  unipwr  42460  supxrre3  42871  fsumiunss  43123  rrpsscn  43136  dvnmul  43491  dvnprodlem2  43495  stoweidlem34  43582  stirlinglem13  43634  fourierdlem20  43675  fourierdlem62  43716  fourierdlem83  43737  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fouriersw  43779  qndenserrnbllem  43842  sge0iunmptlemre  43960  nn0ssge0  43969  sge0isum  43972  sge0seq  43991  sge0reuz  43992  caragendifcl  44059  carageniuncllem2  44067  hoicvrrex  44101  smfaddlem1  44308  smfaddlem2  44309  mbfpsssmf  44328  ringssrng  45449  srhmsubc  45645  srhmsubcALTV  45663  lvecpsslmod  45859  thincssc  46318  aacllem  46516  amgmwlem  46517  amgmlemALT  46518  upwordsseti  46531