Theorem ssriv 3802

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

Syntax hints:   → wi 4   ∈ wcel 2156   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783

This theorem is referenced by:  ssid  3820  ssv  3822  difss  3936  ssun1  3975  inss1  4029  0ss  4170  difprsnss  4520  snsspw  4563  uniin  4652  pwuni  4668  iuniin  4723  iunpwss  4810  pwunss  5214  relopabi  5447  dmin  5533  dmrnssfld  5585  dmcoss  5586  dminss  5758  imainss  5759  fviss  6477  mapsspm  8126  pmsspw  8127  uniixp  8168  pwfilem  8499  dffi3  8576  dfom3  8791  onwf  8940  tcrank  8994  djuss  9029  djuunxp  9030  djuun  9035  cardprclem  9088  alephsson  9206  ackbij1  9345  cardcf  9359  cfeq0  9363  dfacfin7  9506  hsmexlem6  9538  canthnum  9756  inaprc  9943  nqerf  10037  addnqf  10055  mulnqf  10056  dmrecnq  10075  reclem2pr  10155  wuncn  10276  zssre  11650  zsscn  11651  nnssz  11663  elq  12009  zssq  12014  qssre  12017  rpssre  12057  ixxssixx  12407  iooval2  12426  ioossre  12453  rge0ssre  12500  fzssz  12566  fz1ssnn  12595  fzssuz  12605  fzssp1  12607  uzdisj  12636  fz0ssnn0  12658  nn0disj  12679  fzossfz  12712  fzouzsplit  12727  fzossnn  12741  fzo0ssnn0  12773  uzrdgfni  12981  seqcoll  13465  wrdexg  13526  wrdexb  13527  fclim  14507  isercolllem3  14620  isercoll  14621  climcnds  14805  divcnv  14807  harmonic  14813  fprodge0  14944  bitsss  15367  prmssnn  15608  maxprmfct  15638  prminf  15836  prmreclem3  15839  1arithlem1  15844  1arith  15848  4sqlem19  15884  vdwlem12  15913  restsspw  16297  xpsc0  16425  xpsc1  16426  mremre  16469  mreacs  16523  isfunc  16728  homarel  16890  ledm  17429  lern  17430  sgrpssmgm  17625  mndsssgrp  17626  prdsgrpd  17730  prdsinvgd  17731  symgtrf  18090  odf1o2  18189  sylow3lem3  18245  sylow3lem6  18248  oppglsm  18258  efgsfo  18353  0frgp  18393  prdscmnd  18465  prdsabld  18466  dprdssv  18617  dprdres  18629  ablfac1b  18671  prdsringd  18814  prdscrngd  18815  unitss  18862  subrgint  19006  lssintcl  19171  prdslmodd  19176  xrge0subm  19995  cnsubmlem  20002  cnsubglem  20003  cnsubdrglem  20005  cnmsubglem  20017  zringunit  20044  zringlpir  20045  znf1o  20107  zntoslem  20112  ocvss  20224  dsmmsubg  20297  dsmmlss  20298  lbslinds  20382  unitg  20985  cldss2  21048  indiscld  21109  toponmre  21111  iscldtop  21113  1stcfb  21462  llyssnlly  21495  llyidm  21505  nllyidm  21506  toplly  21507  hauslly  21509  lly1stc  21513  dissnref  21545  1stckgenlem  21570  txindis  21651  pthaus  21655  ptcmpfi  21830  ufinffr  21946  cnflf2  22020  flimfcls  22043  alexsubALTlem3  22066  ptcmplem1  22069  ptcmpg  22074  prdstmdd  22140  prdstgpd  22141  ust0  22236  prdsms  22549  qdensere  22786  blssioo  22811  tgioo  22812  xrtgioo  22822  xrsmopn  22828  zdis  22832  reperflem  22834  xrge0gsumle  22849  xrge0tsms  22850  icopnfhmeo  22955  bndth  22970  ovoliunlem1  23483  ovoliun2  23487  ovolicc2lem4  23501  voliunlem2  23532  voliunlem3  23533  uniioovol  23560  uniioombllem4  23567  vitali  23594  ismbf3d  23635  itg2seq  23723  limccl  23853  limcresi  23863  dvef  23957  aasscn  24287  qssaa  24293  aannenlem2  24298  aannenlem3  24299  ulmcn  24367  mtestbdd  24373  iblulm  24375  reeff1o  24415  reefgim  24418  efifo  24508  dfrelog  24526  relogf1o  24527  logdmss  24602  logcn  24607  dvloglem  24608  logf1o2  24610  dvlog  24611  dvlog2lem  24612  dvlog2  24613  logtayl  24620  cxpcn  24700  cxpcn2  24701  cxpcn3  24703  resqrtcn  24704  efrlim  24910  dfef2  24911  cxp2lim  24917  wilthlem2  25009  wilthlem3  25010  basellem3  25023  basellem4  25024  prmdvdsfi  25047  vmaval  25053  mumul  25121  sqff1o  25122  musum  25131  fsumvma2  25153  dchrmhm  25180  chtppilim  25378  chto1lb  25381  chpchtlim  25382  chpo1ub  25383  dchrisumlema  25391  dchrmusum2  25397  dchrvmasum2lem  25399  dirith2  25431  mudivsum  25433  mulogsum  25435  mulog2sumlem2  25438  selberg2lem  25453  selberg3lem2  25461  pntrsumo1  25468  pnt2  25516  pnt  25517  axcontlem2  26059  usgrexmplef  26367  griedg0ssusgr  26373  nbgrssvtx  26452  nbgrssovtx  26473  uvtxssvtx  26510  rgrusgrprc  26713  clwlkswks  26900  wwlkssswrd  26989  wwlkssswwlksn  26993  wspthsswwlkn  27058  wspthsswwlknon  27061  clwwlksclwwlkn  27179  phrel  27998  bnrel  28051  hlrel  28074  shex  28397  chsssh  28410  hhssnv  28449  choc1  28514  shunssi  28555  shsleji  28557  shsub1i  28559  shsub2i  28560  shsidmi  28571  omlsii  28590  spanuni  28731  spansni  28744  5oalem7  28847  3oalem3  28851  pjrni  28889  mayete3i  28915  hmopex  29062  cnlnssadj  29267  adjbdln  29270  adjsslnop  29274  shatomistici  29548  hatomistici  29549  xrge0tsmsd  30110  esumpcvgval  30465  hashf2  30471  insiga  30525  sigapisys  30543  sigaldsys  30547  sigapildsys  30550  sxbrsigalem0  30658  dya2icobrsiga  30663  sxbrsigalem1  30672  sxbrsigalem2  30673  eulerpartlemb  30755  chtvalz  31032  logdivsqrle  31053  bnj1398  31425  bnj1498  31452  erdszelem9  31504  erdsze2lem2  31509  kur14lem9  31519  ptpconn  31538  iinllyconn  31559  cvmlift3  31633  mppsthm  31799  imagesset  32381  altxpsspw  32405  topjoin  32681  onsstopbas  32745  onsucconni  32753  onintopssconn  32756  onint1  32765  oninhaus  32766  bj-snglss  33268  bj-modssabl  33459  icoreunrn  33523  poimirlem8  33730  poimirlem18  33740  poimirlem21  33743  poimirlem22  33744  poimirlem31  33753  poimirlem32  33754  heiborlem3  33923  atssbase  35070  eldioph3b  37830  diophin  37838  diophun  37839  eldiophss  37840  isnumbasabl  38177  isnumbasgrp  38178  dfacbasgrp  38179  mon1psubm  38285  inintabss  38384  intimass  38446  nzin  39017  unipwrVD  39561  unipwr  39562  supxrre3  40021  fsumiunss  40287  rrpsscn  40300  dvnmul  40638  dvnprodlem2  40642  stoweidlem34  40730  stirlinglem13  40782  fourierdlem20  40823  fourierdlem62  40864  fourierdlem83  40885  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fouriersw  40927  qndenserrnbllem  40993  sge0iunmptlemre  41111  nn0ssge0  41120  sge0isum  41123  sge0seq  41142  sge0reuz  41143  caragendifcl  41210  carageniuncllem2  41218  hoicvrrex  41252  smfaddlem1  41453  smfaddlem2  41454  mbfpsssmf  41473  ringssrng  42448  srhmsubc  42644  srhmsubcALTV  42662  lvecpsslmod  42864  aacllem  43118  amgmwlem  43119  amgmlemALT  43120