Theorem ssriv 3921

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssid  3939  ssv  3941  ssrab2  4009  difss  4062  ssun1  4102  inss1  4159  0ss  4327  difprsnss  4729  snsspw  4772  uniin  4862  pwuni  4875  iuniin  4933  iunpwss  5032  pwunssOLD  5475  relopabi  5721  dmin  5809  dmrnssfld  5868  dmcoss  5869  dminss  6045  imainss  6046  fviss  6827  mapfoss  8598  fsetsspwxp  8599  mapsspm  8622  pmsspw  8623  uniixp  8667  pwfilem  8922  pwfilemOLD  9043  dffi3  9120  dfom3  9335  onwf  9519  tcrank  9573  djuss  9609  djuunxp  9610  djuun  9615  cardprclem  9668  alephsson  9787  ackbij1  9925  cardcf  9939  cfeq0  9943  dfacfin7  10086  hsmexlem6  10118  canthnum  10336  inaprc  10523  nqerf  10617  addnqf  10635  mulnqf  10636  dmrecnq  10655  reclem2pr  10735  wuncn  10857  zssre  12256  zsscn  12257  nnssz  12270  elq  12619  zssq  12625  qssre  12628  ixxssixx  13022  iooval2  13041  ioossre  13069  rge0ssre  13117  fzssz  13187  fz1ssnn  13216  fzssuz  13226  fzssp1  13228  uzdisj  13258  fz0ssnn0  13280  nn0disj  13301  fzossfz  13334  fzouzsplit  13350  fzo0ssnn0  13396  uzrdgfni  13606  seqcoll  14106  wrdexb  14156  fclim  15190  isercolllem3  15306  climcnds  15491  divcnv  15493  harmonic  15499  bitsss  16061  prmssnn  16309  maxprmfct  16342  1arith  16556  4sqlem19  16592  vdwlem12  16621  restsspw  17059  mremre  17230  mreacs  17284  isfunc  17495  homarel  17667  ledm  18223  lern  18224  smndex1basss  18459  sgrpssmgm  18487  mndsssgrp  18488  prdsgrpd  18600  prdsinvgd  18601  symgpssefmnd  18918  symgsubmefmndALT  18926  pgrpsubgsymg  18932  symgtrf  18992  odf1o2  19093  sylow3lem3  19149  sylow3lem6  19152  oppglsm  19162  efgsfo  19260  0frgp  19300  prdscmnd  19377  prdsabld  19378  dprdssv  19534  dprdres  19546  prdsringd  19766  prdscrngd  19767  unitss  19817  subrgint  19961  subdrgint  19986  sdrgint  19987  primefld  19988  lssintcl  20141  prdslmodd  20146  xrge0subm  20551  cnsubmlem  20558  cnsubglem  20559  cnsubdrglem  20561  cnmsubglem  20573  zringunit  20600  zringlpir  20601  znf1o  20671  ocvss  20787  dsmmsubg  20860  dsmmlss  20861  lbslinds  20950  unitg  22025  cldss2  22089  indiscld  22150  iscldtop  22154  llyssnlly  22537  llyidm  22547  nllyidm  22548  toplly  22549  hauslly  22551  lly1stc  22555  dissnref  22587  txindis  22693  pthaus  22697  ptcmpfi  22872  ufinffr  22988  cnflf2  23062  flimfcls  23085  alexsubALTlem3  23108  ptcmplem1  23111  ptcmpg  23116  prdstmdd  23183  prdstgpd  23184  ust0  23279  prdsms  23593  qdensere  23839  blssioo  23864  tgioo  23865  xrtgioo  23875  xrsmopn  23881  zdis  23885  reperflem  23887  xrge0gsumle  23902  xrge0tsms  23903  icopnfhmeo  24012  bndth  24027  voliunlem2  24620  voliunlem3  24621  vitali  24682  ismbf3d  24723  itg2seq  24812  limccl  24944  limcresi  24954  dvef  25049  aasscn  25383  qssaa  25389  aannenlem2  25394  aannenlem3  25395  ulmcn  25463  mtestbdd  25469  iblulm  25471  reeff1o  25511  reefgim  25514  efifo  25608  dfrelog  25626  relogf1o  25627  logdmss  25702  logcn  25707  dvloglem  25708  logf1o2  25710  dvlog  25711  dvlog2lem  25712  dvlog2  25713  logtayl  25720  cxpcn  25803  cxpcn2  25804  cxpcn3  25806  resqrtcn  25807  efrlim  26024  dfef2  26025  cxp2lim  26031  basellem3  26137  basellem4  26138  sqff1o  26236  dchrmhm  26294  chtppilim  26528  chto1lb  26531  chpchtlim  26532  chpo1ub  26533  dchrisumlema  26541  selberg2lem  26603  selberg3lem2  26611  pntrsumo1  26618  pnt2  26666  pnt  26667  axcontlem2  27236  usgrexmplef  27529  griedg0ssusgr  27535  nbgrssvtx  27612  nbgrssovtx  27631  uvtxssvtx  27660  rgrusgrprc  27859  clwlkswks  28045  wwlkssswrd  28128  wwlkssswwlksn  28132  wspthsswwlkn  28184  wspthsswwlknon  28187  clwwlksclwwlkn  28296  phrel  29078  bnrel  29130  hlrel  29153  shex  29475  chsssh  29488  hhssnv  29527  choc1  29590  shunssi  29631  shsleji  29633  shsub1i  29635  shsub2i  29636  shsidmi  29647  omlsii  29666  spanuni  29807  spansni  29820  5oalem7  29923  3oalem3  29927  pjrni  29965  mayete3i  29991  hmopex  30138  cnlnssadj  30343  adjbdln  30346  adjsslnop  30350  shatomistici  30624  hatomistici  30625  xrge0tsmsd  31219  primefldchr  31395  esumpcvgval  31946  hashf2  31952  insiga  32005  sigapisys  32023  sigaldsys  32027  sigapildsys  32030  sxbrsigalem0  32138  dya2icobrsiga  32143  sxbrsigalem1  32152  sxbrsigalem2  32153  eulerpartlemb  32235  chtvalz  32509  logdivsqrle  32530  bnj1398  32914  bnj1498  32941  fineqvacALT  32967  erdszelem9  33061  erdsze2lem2  33066  kur14lem9  33076  ptpconn  33095  iinllyconn  33116  cvmlift3  33190  mppsthm  33441  madef  33967  imagesset  34182  altxpsspw  34206  topjoin  34481  onsstopbas  34545  onsucconni  34553  onintopssconn  34556  onint1  34565  oninhaus  34566  bj-snglss  35087  bj-imdirco  35288  bj-modssabl  35378  bj-rvecssmod  35394  bj-rvecssvec  35399  bj-rvecsscmod  35401  icoreunrn  35457  difunieq  35472  poimirlem8  35712  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem31  35735  poimirlem32  35736  heiborlem3  35898  atssbase  37231  eldioph3b  40503  diophin  40510  diophun  40511  eldiophss  40512  isnumbasabl  40847  isnumbasgrp  40848  dfacbasgrp  40849  mon1psubm  40947  inintabss  41075  intimass  41151  inaex  41804  nzin  41825  unipwrVD  42341  unipwr  42342  supxrre3  42754  fsumiunss  43006  rrpsscn  43019  dvnmul  43374  dvnprodlem2  43378  stoweidlem34  43465  stirlinglem13  43517  fourierdlem20  43558  fourierdlem62  43599  fourierdlem83  43620  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fouriersw  43662  qndenserrnbllem  43725  sge0iunmptlemre  43843  nn0ssge0  43852  sge0isum  43855  sge0seq  43874  sge0reuz  43875  caragendifcl  43942  carageniuncllem2  43950  hoicvrrex  43984  smfaddlem1  44185  smfaddlem2  44186  mbfpsssmf  44205  ringssrng  45326  srhmsubc  45522  srhmsubcALTV  45540  lvecpsslmod  45736  thincssc  46195  aacllem  46391  amgmwlem  46392  amgmlemALT  46393