Theorem ssrdv 3975

Description: Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
ssrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
ssrdv	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3957	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 236	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2114   ⊆ wss 3938

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  eqelssd  3990  sscon  4117  ssdif  4118  unss1  4157  ssrin  4212  eq0rdv  4359  sspw  4554  elpwdifsn  4723  uniss  4848  intss1  4893  intmin  4898  intssuni  4900  iinssiun  4934  iunss1  4935  iinss1  4936  ss2iun  4939  ssiun  4972  ssiun2  4973  iinss  4982  iinss2  4983  iunxdif3  5019  sspwb  5344  pwssun  5458  relop  5723  dmss  5773  dmcosseq  5846  ssrnres  6037  sossfld  6045  predpo  6168  preddowncl  6177  tron  6216  tz7.7  6219  dffv2  6758  chfnrn  6821  fvn0ssdmfun  6844  fveqdmss  6848  dff3  6868  ffnfv  6884  f1imass  7024  ssorduni  7502  onint  7512  limsssuc  7567  limuni3  7569  limomss  7587  fo1stres  7717  fo2ndres  7718  fo2ndf  7819  fnse  7829  ressuppssdif  7853  suppss  7862  reldmtpos  7902  onfununi  7980  smoiun  8000  smorndom  8007  tz7.48-1  8081  tz7.49  8083  oaass  8189  qsss  8360  uniinqs  8379  pmss12g  8435  mapss  8455  ixpssmap2g  8493  ixpssmapg  8494  fineqv  8735  pssnn  8738  ssfii  8885  dffi2  8889  oismo  9006  unxpwdom2  9054  inf3lemd  9092  inf3lem1  9093  inf3lem6  9098  cantnflem3  9156  cantnf  9158  cnfcom3lem  9168  onssr1  9262  rankunb  9281  tcrank  9315  harcard  9409  carduni  9412  infxpenlem  9441  infpwfien  9490  dfac12r  9574  ackbij2lem1  9643  ackbij1lem18  9661  isfin1-3  9810  fin1a2lem11  9834  fin1a2lem13  9836  zorn2lem4  9923  zorn2lem5  9924  ttukeylem6  9938  ttukeylem7  9939  fpwwe2lem11  10064  fpwwe2lem12  10065  fpwwe2  10067  wunr1om  10143  wunom  10144  tskr1om  10191  tskr1om2  10192  tskxpss  10196  tskcard  10205  tskuni  10207  grothomex  10253  genpss  10428  distrlem1pr  10449  distrlem5pr  10451  ltexprlem2  10461  ltexprlem6  10465  ltexprlem7  10466  reclem3pr  10473  reclem4pr  10474  supaddc  11610  supadd  11611  supmul1  11612  supmullem2  11614  peano5uzi  12074  uzss  12268  ixxdisj  12756  ixxss1  12759  ixxss2  12760  ixxss12  12761  ixxub  12762  ixxlb  12763  iocssre  12819  icossre  12820  iccssre  12821  icodisj  12865  fzss1  12949  fzss2  12950  ssfzunsnext  12955  fzosplit  13073  fzouzsplit  13075  ssfzo12bi  13135  ssnn0fi  13356  fsuppmapnn0fiub  13362  suppssfz  13365  sswrd  13872  rtrclreclem3  14421  isercoll  15026  summolem2a  15074  fsumcvg3  15088  fsum2dlem  15127  fsumcom2  15131  qshash  15184  prodmolem2a  15290  fprod2dlem  15336  fprodcom2  15340  bitsfzo  15786  1arith  16265  vdwlem2  16320  vdwlem6  16324  vdwlem8  16326  ramtlecl  16338  prmgaplem3  16391  prmgaplem4  16392  monhom  17007  epihom  17014  funcsetcres2  17355  funcestrcsetclem8  17399  funcsetcestrclem8  17414  psdmrn  17819  gsumwspan  18013  frmdss2  18030  sursubmefmnd  18063  injsubmefmnd  18064  trivsubgsnd  18308  ssnmz  18320  trivnsgd  18326  conjnmz  18394  symgvalstruct  18527  gex1  18718  sylow2alem1  18744  lsmless1x  18771  lsmless2x  18772  lsmub1x  18773  lsmub2x  18774  lsmmod  18803  lsmdisj2  18810  efgrelexlemb  18878  efgcpbllemb  18883  cntzcmn  18962  gsum2d2  19096  dprdub  19149  dprdss  19153  dprddisj2  19163  pgpfac1lem3  19201  kerf1ghm  19499  kerf1hrmOLD  19500  isdrng2  19514  subrguss  19552  subrgmre  19561  primefld0cl  19587  primefld1cl  19588  lssssr  19727  lsssssubg  19732  lssmre  19740  lbspss  19856  lspdisj  19899  lbsextlem2  19933  lidl1el  19993  drngnidl  20004  lpiss  20025  unitrrg  20068  mhpsubg  20342  zsssubrg  20605  qsssubdrg  20606  cnsubrg  20607  mulgrhm2  20648  znrrg  20714  ocvocv  20817  ocv2ss  20819  ocvin  20820  lsmcss  20838  cssmre  20839  pjcss  20862  lindfrn  20967  dmatsgrp  21110  scmatsgrp  21130  scmatsgrp1  21133  m2cpmrngiso  21368  bastg  21576  tgss  21578  tgtop  21583  tgidm  21590  en2top  21595  neisspw  21717  topssnei  21734  neiptopuni  21740  lpss3  21754  clslp  21758  tgrest  21769  ssrest  21786  restntr  21792  ordtbas2  21801  ordtbas  21802  cnss1  21886  cnss2  21887  cnsscnp  21889  cnrest2r  21897  cmpsublem  22009  cmpsub  22010  tgcmp  22011  cmpcld  22012  hauscmplem  22016  cnconn  22032  llyss  22089  nllyss  22090  restnlly  22092  restlly  22093  locfincmp  22136  locfincf  22141  kgenss  22153  kgenidm  22157  llycmpkgen2  22160  1stckgen  22164  kgen2ss  22165  kgencn3  22168  ptbasfi  22191  ptpjopn  22222  txdis  22242  txkgen  22262  xkoptsub  22264  xkopjcn  22266  txconn  22299  qtoptop2  22309  qtopuni  22312  qtopkgen  22320  basqtop  22321  tgqtop  22322  qtopss  22325  qtoprest  22327  qtopomap  22328  qtopcmap  22329  kqsat  22341  kqcldsat  22343  hmphdis  22406  isfild  22468  ssfg  22482  fgss  22483  fgss2  22484  fgfil  22485  fgabs  22489  filconn  22493  fgtr  22500  uzrest  22507  ufilmax  22517  ufileu  22529  filufint  22530  rnelfm  22563  fmfnfmlem2  22565  fmfnfmlem4  22567  flimss2  22582  flimss1  22583  flimclsi  22588  flimcf  22592  flimsncls  22596  fclssscls  22628  fclsss1  22632  fclsss2  22633  fclscf  22635  uffclsflim  22641  alexsublem  22654  alexsubALTlem3  22659  ptcmplem2  22663  ptcmplem3  22664  cnextf  22676  efmndtmd  22711  symgtgp  22716  cldsubg  22721  tsmscl  22745  haustsms2  22747  tgptsmscls  22760  tsmsxp  22765  restutop  22848  ustuqtop4  22855  utop2nei  22861  utop3cls  22862  ucncn  22896  xblss2ps  23013  xblss2  23014  xrsblre  23421  xrsmopn  23422  recld2  23424  zdis  23426  icccmplem2  23433  cncfss  23509  cnheiborlem  23560  htpycn  23579  phtpyhtpy  23588  pi1blem  23645  cphsscph  23856  cfilfcls  23879  iscmet3lem2  23897  iscmet2  23899  caussi  23902  equivcfil  23904  lmcau  23918  metsscmetcld  23920  hlhil  24048  ivthicc  24061  ovoliunnul  24110  ovolicopnf  24127  uniioombllem3  24188  dyadmbllem  24202  volsup2  24208  vitalilem2  24212  itg1addlem4  24302  itg10a  24313  itg1ge0a  24314  mbfi1fseqlem4  24321  itg2gt0  24363  limciun  24494  perfdvf  24503  cpnord  24534  dvcj  24549  dvlip2  24594  dvivth  24609  dvne0  24610  dvcnvre  24618  ply1lpir  24774  plyco0  24784  plyexmo  24904  abelth  25031  efif1o  25132  logno1  25221  efopnlem2  25242  loglesqrt  25341  lgamcvg2  25634  ppisval  25683  ppinprm  25731  chtnprm  25733  fsumvma  25791  dchrfi  25833  chtppilimlem2  26052  chebbnd2  26055  vmadivsumb  26061  rplogsumlem2  26063  dchrisumlem2  26068  vmalogdivsum2  26116  vmalogdivsum  26117  2vmadivsumlem  26118  selbergb  26127  selberg2b  26130  selberg3lem1  26135  selberg3lem2  26136  selberg3  26137  selberg4lem1  26138  selberg4  26139  pntrlog2bndlem2  26156  pntrlog2bndlem4  26158  uhgredgss  26918  usgruspgrb  26968  uhgrissubgr  27059  uhgrspansubgrlem  27074  uhgrspan1  27087  cusgredg  27208  usgredgsscusgredg  27243  ococss  29072  shsub1  29103  shless  29138  shmodsi  29168  pjhth  29172  spansnss  29350  spanpr  29359  spansnm0i  29429  pjjsi  29479  sumdmdii  30194  sumdmdlem  30197  sumdmdlem2  30198  cdj3lem1  30213  abrexss  30274  fnpreimac  30418  rnmposs  30421  unifi3  30450  uzssico  30509  ssnnssfz  30512  pmtrcnel  30735  cycpmrn  30787  cyc3evpm  30794  cycpmgcl  30797  dimkerim  31025  extdg1id  31055  crefss  31115  cmpcref  31116  tpr2rico  31157  esumrnmpt2  31329  esumpcvgval  31339  ldsysgenld  31421  sigapildsys  31423  ldgenpisys  31427  cldssbrsiga  31448  measdivcstALTV  31486  mbfmcnt  31528  oddpwdc  31614  eulerpartlemgs2  31640  reprpmtf1o  31899  bnj1033  32243  bnj1398  32308  sconnpi1  32488  cvmscld  32522  cvmliftlem15  32547  satfrnmapom  32619  dfon2lem6  33035  fprlem2  33140  fnessref  33707  fgmin  33720  tailfb  33727  dissneqlem  34623  icoreresf  34635  rdglimss  34660  finxpreclem6  34679  lindsenlbs  34889  poimirlem11  34905  poimirlem12  34906  sstotbnd3  35056  prdstotbnd  35074  cntotbnd  35076  ismtyhmeo  35085  1idl  35306  lshpdisj  36125  lssats  36150  lkrin  36302  glbconxN  36516  paddss1  36955  paddss2  36956  paddasslem16  36973  paddidm  36979  pmodlem2  36985  pmapjoin  36990  pmapjat1  36991  pclfinN  37038  pclfinclN  37088  diasslssN  38197  dia2dimlem12  38213  dihsslss  38414  baerlem3lem2  38848  baerlem5alem2  38849  baerlem5blem2  38850  eldiophss  39378  rencldnfilem  39424  pellexlem5  39437  pell14qrss1234  39460  pell1qrss14  39472  pellfundre  39485  pellfundge  39486  pellfundlb  39488  pellfundglb  39489  harinf  39638  proot1hash  39807  intabssd  39892  ss2iundf  40011  ov2ssiunov2  40052  clsk1indlem3  40400  radcnvrat  40653  nznngen  40655  trsspwALT3  41161  sspwimpALT2  41269  refsumcn  41294  iinssf  41414  icoiccdif  41807  icccncfext  42177  stoweidlem27  42319  stoweidlem46  42338  stoweidlem57  42349  fourierdlem40  42439  fourierdlem78  42476  ffnafv  43377  iccpartrn  43597  sprsymrelfvlem  43659  sprsymrelf1lem  43660  rnghmsscmap2  44251  rnghmsscmap  44252  funcrngcsetc  44276  funcrngcsetcALT  44277  rhmsscmap2  44297  rhmsscmap  44298  rhmsscrnghm  44304  rngcresringcat  44308  funcringcsetc  44313  funcringcsetcALTV2lem8  44321  funcringcsetclem8ALTV  44344  rhmsubcALTVlem4  44385  ssnn0ssfz  44404  lincolss  44496  lcoss  44498  lcosslsp  44500  iunord  44786