Theorem ssriv 3936

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  ssid  3954  ssv  3956  ssrab2  4025  difss  4079  ssun1  4120  inss1  4176  0ss  4344  difprsnss  4747  snsspw  4790  uniin  4880  pwuni  4894  iuniin  4954  iunpwss  5055  relopabi  5765  dmin  5854  dmrnssfld  5912  dmcoss  5913  dminss  6092  imainss  6093  fvssunirn  6859  fviss  6902  opabresex2  7390  fvmptopab  7392  mapfoss  8712  fsetsspwxp  8713  mapsspm  8736  pmsspw  8737  uniixp  8781  pwfilem  9043  pwfilemOLD  9212  dffi3  9289  dfom3  9505  onwf  9688  tcrank  9742  djuss  9778  djuunxp  9779  djuun  9784  cardprclem  9837  alephsson  9958  ackbij1  10096  cardcf  10110  cfeq0  10114  dfacfin7  10257  hsmexlem6  10289  canthnum  10507  inaprc  10694  nqerf  10788  addnqf  10806  mulnqf  10807  dmrecnq  10826  reclem2pr  10906  wuncn  11028  zssre  12428  zsscn  12429  nnssz  12442  elq  12792  zssq  12798  qssre  12801  ixxssixx  13195  iooval2  13214  ioossre  13242  rge0ssre  13290  fzssz  13360  fz1ssnn  13389  fzssuz  13399  fzssp1  13401  uzdisj  13431  fz0ssnn0  13453  nn0disj  13474  fzossfz  13508  fzouzsplit  13524  fzo0ssnn0  13570  uzrdgfni  13780  seqcoll  14279  wrdexb  14329  fclim  15362  isercolllem3  15478  climcnds  15663  divcnv  15665  harmonic  15671  bitsss  16233  prmssnn  16479  maxprmfct  16512  1arith  16726  4sqlem19  16762  vdwlem12  16791  restsspw  17240  mremre  17411  mreacs  17465  isfunc  17677  homarel  17849  ledm  18406  lern  18407  smndex1basss  18641  sgrpssmgm  18669  mndsssgrp  18670  prdsgrpd  18782  prdsinvgd  18783  symgpssefmnd  19100  symgsubmefmndALT  19108  pgrpsubgsymg  19114  symgtrf  19174  odf1o2  19275  sylow3lem3  19331  sylow3lem6  19334  oppglsm  19344  efgsfo  19441  0frgp  19481  prdscmnd  19558  prdsabld  19559  dprdssv  19715  dprdres  19727  prdsringd  19947  prdscrngd  19948  unitss  19998  subrgint  20152  subdrgint  20178  sdrgint  20179  primefld  20180  lssintcl  20333  prdslmodd  20338  xrge0subm  20746  cnsubmlem  20753  cnsubglem  20754  cnsubdrglem  20756  cnmsubglem  20768  zringunit  20795  zringlpir  20796  znf1o  20866  ocvss  20982  dsmmsubg  21057  dsmmlss  21058  lbslinds  21147  unitg  22224  cldss2  22288  indiscld  22349  iscldtop  22353  llyssnlly  22736  llyidm  22746  nllyidm  22747  toplly  22748  hauslly  22750  lly1stc  22754  dissnref  22786  txindis  22892  pthaus  22896  ptcmpfi  23071  ufinffr  23187  cnflf2  23261  flimfcls  23284  alexsubALTlem3  23307  ptcmplem1  23310  ptcmpg  23315  prdstmdd  23382  prdstgpd  23383  ust0  23478  prdsms  23794  qdensere  24040  blssioo  24065  tgioo  24066  xrtgioo  24076  xrsmopn  24082  zdis  24086  reperflem  24088  xrge0gsumle  24103  xrge0tsms  24104  icopnfhmeo  24213  bndth  24228  voliunlem2  24822  voliunlem3  24823  vitali  24884  ismbf3d  24925  itg2seq  25014  limccl  25146  limcresi  25156  dvef  25251  aasscn  25585  qssaa  25591  aannenlem2  25596  aannenlem3  25597  ulmcn  25665  mtestbdd  25671  iblulm  25673  reeff1o  25713  reefgim  25716  efifo  25810  dfrelog  25828  relogf1o  25829  logdmss  25904  logcn  25909  dvloglem  25910  logf1o2  25912  dvlog  25913  dvlog2lem  25914  dvlog2  25915  logtayl  25922  cxpcn  26005  cxpcn2  26006  cxpcn3  26008  resqrtcn  26009  efrlim  26226  dfef2  26227  cxp2lim  26233  basellem3  26339  basellem4  26340  sqff1o  26438  dchrmhm  26496  chtppilim  26730  chto1lb  26733  chpchtlim  26734  chpo1ub  26735  dchrisumlema  26743  selberg2lem  26805  selberg3lem2  26813  pntrsumo1  26820  pnt2  26868  pnt  26869  axcontlem2  27623  usgrexmplef  27916  griedg0ssusgr  27922  nbgrssvtx  27999  nbgrssovtx  28018  uvtxssvtx  28047  rgrusgrprc  28246  clwlkswks  28433  wwlkssswrd  28516  wwlkssswwlksn  28520  wspthsswwlkn  28572  wspthsswwlknon  28575  clwwlksclwwlkn  28684  phrel  29466  bnrel  29518  hlrel  29541  shex  29863  chsssh  29876  hhssnv  29915  choc1  29978  shunssi  30019  shsleji  30021  shsub1i  30023  shsub2i  30024  shsidmi  30035  omlsii  30054  spanuni  30195  spansni  30208  5oalem7  30311  3oalem3  30315  pjrni  30353  mayete3i  30379  hmopex  30526  cnlnssadj  30731  adjbdln  30734  adjsslnop  30738  shatomistici  31012  hatomistici  31013  xrge0tsmsd  31604  primefldchr  31782  1fldgenq  31793  esumpcvgval  32344  hashf2  32350  insiga  32403  sigapisys  32421  sigaldsys  32425  sigapildsys  32428  sxbrsigalem0  32538  dya2icobrsiga  32543  sxbrsigalem1  32552  sxbrsigalem2  32553  eulerpartlemb  32635  chtvalz  32909  logdivsqrle  32930  bnj1398  33313  bnj1498  33340  fineqvacALT  33366  erdszelem9  33460  erdsze2lem2  33465  kur14lem9  33475  ptpconn  33494  iinllyconn  33515  cvmlift3  33589  mppsthm  33840  madef  34150  imagesset  34394  altxpsspw  34418  topjoin  34693  onsstopbas  34757  onsucconni  34765  onintopssconn  34768  onint1  34777  oninhaus  34778  bj-snglss  35297  bj-imdirco  35517  bj-modssabl  35607  bj-rvecssmod  35623  bj-rvecssvec  35628  bj-rvecsscmod  35630  icoreunrn  35686  difunieq  35701  poimirlem8  35941  poimirlem18  35951  poimirlem21  35954  poimirlem22  35955  poimirlem31  35964  poimirlem32  35965  heiborlem3  36127  atssbase  37608  eldioph3b  40900  diophin  40907  diophun  40908  eldiophss  40909  isnumbasabl  41245  isnumbasgrp  41246  dfacbasgrp  41247  mon1psubm  41345  omssrncard  41521  inintabss  41559  intimass  41635  inaex  42288  nzin  42309  unipwrVD  42825  unipwr  42826  supxrre3  43251  fsumiunss  43504  rrpsscn  43517  dvnmul  43872  dvnprodlem2  43876  stoweidlem34  43963  stirlinglem13  44015  fourierdlem20  44056  fourierdlem62  44097  fourierdlem83  44118  fourierdlem101  44136  fourierdlem103  44138  fourierdlem104  44139  fourierdlem111  44146  fouriersw  44160  qndenserrnbllem  44223  sge0iunmptlemre  44342  nn0ssge0  44351  sge0isum  44354  sge0seq  44373  sge0reuz  44374  caragendifcl  44441  carageniuncllem2  44449  hoicvrrex  44483  smfaddlem1  44690  smfaddlem2  44691  mbfpsssmf  44710  upwordsseti  44802  ringssrng  45856  srhmsubc  46052  srhmsubcALTV  46070  lvecpsslmod  46266  thincssc  46725  aacllem  46923  amgmwlem  46924  amgmlemALT  46925