Theorem ssriv 3572

Description: Inference rule 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 3557	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1717	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  ssid  3587  ssv  3588  difss  3699  ssun1  3738  inss1  3795  0ss  3924  difprsnss  4270  snsspw  4315  uniin  4393  iuniin  4467  iunpwss  4551  pwuni  4825  pwunss  4943  relopabi  5167  dmin  5254  dmrnssfld  5305  dmcoss  5306  dminss  5466  imainss  5467  fviss  6166  mapsspm  7777  pmsspw  7778  uniixp  7817  pwfilem  8143  dffi3  8220  dfom3  8427  onwf  8576  tcrank  8630  cardprclem  8688  alephsson  8806  ackbij1  8943  cardcf  8957  cfeq0  8961  dfacfin7  9104  hsmexlem6  9136  canthnum  9350  inaprc  9537  nqerf  9631  addnqf  9649  mulnqf  9650  dmrecnq  9669  reclem2pr  9749  wuncn  9870  zssre  11261  zsscn  11262  nnssz  11274  elq  11666  zssq  11671  qssre  11674  rpssre  11719  ixxssixx  12060  iooval2  12079  ioossre  12106  rge0ssre  12151  fzssz  12214  fz1ssnn  12243  fzssuz  12253  fzssp1  12255  uzdisj  12282  fz0ssnn0  12304  nn0disj  12324  fzossfz  12357  fzouzsplit  12372  fzossnn  12384  fzo0ssnn0  12415  fzo0ssnn0OLD  12416  uzrdgfni  12619  seqcoll  13105  wrdexg  13170  wrdexb  13171  fclim  14132  isercolllem3  14245  isercoll  14246  climcnds  14422  divcnv  14424  harmonic  14430  fprodge0  14563  bitsss  14986  prmssnn  15228  maxprmfct  15259  prminf  15457  prmreclem3  15460  1arithlem1  15465  1arith  15469  4sqlem19  15505  vdwlem12  15534  restsspw  15915  xpsc0  16043  xpsc1  16044  mremre  16087  mreacs  16142  isfunc  16347  homarel  16509  ledm  17047  lern  17048  sgrpssmgm  17243  mndsssgrp  17244  prdsgrpd  17348  prdsinvgd  17349  symgtrf  17712  odf1o2  17811  sylow3lem3  17867  sylow3lem6  17870  oppglsm  17880  efgsfo  17975  0frgp  18015  prdscmnd  18087  prdsabld  18088  dprdssv  18238  dprdres  18250  ablfac1b  18292  prdsringd  18435  prdscrngd  18436  unitss  18483  subrgint  18625  lssintcl  18785  prdslmodd  18790  xrge0subm  19606  cnsubmlem  19613  cnsubglem  19614  cnsubdrglem  19616  cnmsubglem  19628  zringunit  19655  zringlpir  19656  znf1o  19719  zntoslem  19724  ocvss  19833  dsmmsubg  19906  dsmmlss  19907  lbslinds  19991  unitg  20582  cldss2  20644  indiscld  20705  toponmre  20707  iscldtop  20709  1stcfb  21058  llyssnlly  21091  llyidm  21101  nllyidm  21102  toplly  21103  hauslly  21105  lly1stc  21109  dissnref  21141  1stckgenlem  21166  txindis  21247  pthaus  21251  ptcmpfi  21426  ufinffr  21543  cnflf2  21617  flimfcls  21640  alexsubALTlem3  21663  ptcmplem1  21666  ptcmpg  21671  prdstmdd  21737  prdstgpd  21738  ust0  21833  prdsms  22146  qdensere  22383  blssioo  22406  tgioo  22407  xrtgioo  22417  xrsmopn  22423  zdis  22427  reperflem  22429  xrge0gsumle  22444  xrge0tsms  22445  icopnfhmeo  22550  bndth  22565  ovoliunlem1  23077  ovoliun2  23081  ovolicc2lem4  23095  voliunlem2  23126  voliunlem3  23127  uniioovol  23153  uniioombllem4  23160  vitali  23188  ismbf3d  23227  itg2seq  23315  limccl  23445  limcresi  23455  dvef  23547  aasscn  23877  qssaa  23883  aannenlem2  23888  aannenlem3  23889  ulmcn  23957  mtestbdd  23963  iblulm  23965  reeff1o  24005  reefgim  24008  efifo  24097  dfrelog  24116  relogf1o  24117  logdmss  24188  logcn  24193  dvloglem  24194  logf1o2  24196  dvlog  24197  dvlog2lem  24198  dvlog2  24199  logtayl  24206  cxpcn  24286  cxpcn2  24287  cxpcn3  24289  resqrtcn  24290  efrlim  24496  dfef2  24497  cxp2lim  24503  wilthlem2  24595  wilthlem3  24596  basellem3  24609  basellem4  24610  prmdvdsfi  24633  vmaval  24639  mumul  24707  sqff1o  24708  musum  24717  fsumvma2  24739  dchrmhm  24766  chtppilim  24964  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  dchrisumlema  24977  dchrmusum2  24983  dchrvmasum2lem  24985  dirith2  25017  mudivsum  25019  mulogsum  25021  mulog2sumlem2  25024  selberg2lem  25039  selberg3lem2  25047  pntrsumo1  25054  pnt2  25102  pnt  25103  axcontlem2  25645  usgraexmplef  25929  wwlksswrd  26216  wwlksswwlkn  26231  clwlksarewlks  26287  phrel  27054  bnrel  27107  hlrel  27130  shex  27453  chsssh  27466  hhssnv  27505  choc1  27570  shunssi  27611  shsleji  27613  shsub1i  27615  shsub2i  27616  shsidmi  27627  omlsii  27646  spanuni  27787  spansni  27800  5oalem7  27903  3oalem3  27907  pjrni  27945  mayete3i  27971  hmopex  28118  cnlnssadj  28323  adjbdln  28326  adjsslnop  28330  shatomistici  28604  hatomistici  28605  xrge0tsmsd  29116  esumpcvgval  29467  hashf2  29473  insiga  29527  sigapisys  29545  sigaldsys  29549  sigapildsys  29552  sxbrsigalem0  29660  dya2icobrsiga  29665  sxbrsigalem1  29674  sxbrsigalem2  29675  eulerpartlemb  29757  bnj1398  30356  bnj1498  30383  erdszelem9  30435  erdsze2lem2  30440  kur14lem9  30450  ptpcon  30469  iinllycon  30490  cvmlift3  30564  mppsthm  30730  imagesset  31230  altxpsspw  31254  topjoin  31530  onsstopbas  31598  onsucconi  31606  onintopsscon  31609  onint1  31618  oninhaus  31619  bj-snglss  32151  bj-modssabl  32319  icoreunrn  32383  poimirlem8  32587  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem31  32610  poimirlem32  32611  heiborlem3  32782  atssbase  33595  eldioph3b  36346  diophin  36354  diophun  36355  eldiophss  36356  isnumbasabl  36695  isnumbasgrp  36696  dfacbasgrp  36697  mon1psubm  36803  inintabss  36903  intimass  36965  nzin  37539  unipwrVD  38089  unipwr  38090  supxrre3  38482  fsumiunss  38642  rrpsscn  38655  dvnmul  38833  dvnprodlem2  38837  stoweidlem34  38927  stirlinglem13  38979  fourierdlem20  39020  fourierdlem62  39061  fourierdlem83  39082  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fouriersw  39124  qndenserrnbllem  39190  sge0iunmptlemre  39308  nn0ssge0  39317  sge0isum  39320  sge0seq  39339  sge0reuz  39340  caragendifcl  39404  carageniuncllem2  39412  hoicvrrex  39446  smfaddlem1  39649  smfaddlem2  39650  mbfpsssmf  39669  griedg0ssusgr  40489  uvtxassvtx  40616  rgrusgrprc  40789  clwlks1wlks  40983  wwlkssswrd  41058  wwlkssswwlksn  41062  wspthsswwlkn  41125  wspthsswwlknon  41128  clwwlkssclwwlksn  41200  ringssrng  41670  srhmsubc  41868  srhmsubcALTV  41887  lvecpsslmod  42090  aacllem  42356  amgmwlem  42357  amgmlemALT  42358