Theorem ssrdv 3866

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 1886	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3848	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 226	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1505   ∈ wcel 2050   ⊆ wss 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-in 3838  df-ss 3845

This theorem is referenced by:  eqelssd  3880  sscon  4007  ssdif  4008  unss1  4045  ssrin  4099  eq0rdv  4244  elpwdifsn  4596  uniss  4734  intss1  4765  intmin  4770  intssuni  4772  iinssiun  4805  iunss1  4806  iinss1  4807  ss2iun  4810  ssiun  4837  ssiun2  4838  iinss  4847  iinss2  4848  iunxdif3  4884  sspwb  5199  pwssun  5309  relop  5572  dmss  5622  dmcosseq  5687  ssrnres  5877  sossfld  5885  predpo  6006  preddowncl  6015  tron  6054  tz7.7  6057  dffv2  6586  chfnrn  6646  fvn0ssdmfun  6669  fveqdmss  6673  dff3  6691  ffnfv  6707  f1imass  6849  ssorduni  7318  onint  7328  limsssuc  7383  limuni3  7385  limomss  7403  fo1stres  7529  fo2ndres  7530  fo2ndf  7624  fnse  7634  ressuppssdif  7656  suppss  7665  reldmtpos  7705  onfununi  7784  smoiun  7804  smorndom  7811  tz7.48-1  7884  tz7.49  7886  oaass  7990  qsss  8160  uniinqs  8179  pmss12g  8235  mapss  8253  ixpssmap2g  8290  ixpssmapg  8291  fineqv  8530  pssnn  8533  ssfii  8680  dffi2  8684  oismo  8801  unxpwdom2  8849  inf3lemd  8886  inf3lem1  8887  inf3lem6  8892  cantnflem3  8950  cantnf  8952  cnfcom3lem  8962  onssr1  9056  rankunb  9075  tcrank  9109  harcard  9203  carduni  9206  infxpenlem  9235  infpwfien  9284  dfac12r  9368  ackbij2lem1  9441  ackbij1lem18  9459  isfin1-3  9608  fin1a2lem11  9632  fin1a2lem13  9634  zorn2lem4  9721  zorn2lem5  9722  ttukeylem6  9736  ttukeylem7  9737  fpwwe2lem11  9862  fpwwe2lem12  9863  fpwwe2  9865  wunr1om  9941  wunom  9942  tskr1om  9989  tskr1om2  9990  tskxpss  9994  tskcard  10003  tskuni  10005  grothomex  10051  genpss  10226  distrlem1pr  10247  distrlem5pr  10249  ltexprlem2  10259  ltexprlem6  10263  ltexprlem7  10264  reclem3pr  10271  reclem4pr  10272  supaddc  11411  supadd  11412  supmul1  11413  supmullem2  11415  peano5uzi  11887  uzss  12082  ixxdisj  12572  ixxss1  12575  ixxss2  12576  ixxss12  12577  ixxub  12578  ixxlb  12579  iocssre  12635  icossre  12636  iccssre  12637  icodisj  12681  fzss1  12765  fzss2  12766  ssfzunsnext  12771  fzosplit  12888  fzouzsplit  12890  ssfzo12bi  12950  ssnn0fi  13171  fsuppmapnn0fiub  13177  suppssfz  13180  sswrd  13683  rtrclreclem3  14283  isercoll  14888  summolem2a  14935  fsumcvg3  14949  fsum2dlem  14988  fsumcom2  14992  qshash  15045  prodmolem2a  15151  fprod2dlem  15197  fprodcom2  15201  bitsfzo  15647  1arith  16122  vdwlem2  16177  vdwlem6  16181  vdwlem8  16183  ramtlecl  16195  prmgaplem3  16248  prmgaplem4  16249  monhom  16866  epihom  16873  funcsetcres2  17214  funcestrcsetclem8  17258  funcsetcestrclem8  17273  psdmrn  17678  gsumwspan  17855  frmdss2  17872  ssnmz  18108  conjnmz  18166  gex1  18480  sylow2alem1  18506  lsmless1x  18533  lsmless2x  18534  lsmub1x  18535  lsmub2x  18536  lsmmod  18562  lsmdisj2  18569  efgrelexlemb  18639  efgcpbllemb  18644  cntzcmn  18721  gsum2d2  18850  dprdub  18900  dprdss  18904  dprddisj2  18914  pgpfac1lem3  18952  kerf1ghm  19223  kerf1hrmOLD  19224  isdrng2  19238  subrguss  19276  subrgmre  19285  primefld0cl  19310  primefld1cl  19311  lssssr  19450  lsssssubg  19455  lssmre  19463  lbspss  19579  lspdisj  19622  lbsextlem2  19656  lidl1el  19715  drngnidl  19726  lpiss  19747  unitrrg  19790  zsssubrg  20308  qsssubdrg  20309  cnsubrg  20310  mulgrhm2  20351  znrrg  20417  ocvocv  20520  ocv2ss  20522  ocvin  20523  lsmcss  20541  cssmre  20542  pjcss  20565  lindfrn  20670  dmatsgrp  20815  scmatsgrp  20835  scmatsgrp1  20838  m2cpmrngiso  21073  bastg  21281  tgss  21283  tgtop  21288  tgidm  21295  en2top  21300  neisspw  21422  topssnei  21439  neiptopuni  21445  lpss3  21459  clslp  21463  tgrest  21474  ssrest  21491  restntr  21497  ordtbas2  21506  ordtbas  21507  cnss1  21591  cnss2  21592  cnsscnp  21594  cnrest2r  21602  cmpsublem  21714  cmpsub  21715  tgcmp  21716  cmpcld  21717  hauscmplem  21721  cnconn  21737  llyss  21794  nllyss  21795  restnlly  21797  restlly  21798  locfincmp  21841  locfincf  21846  kgenss  21858  kgenidm  21862  llycmpkgen2  21865  1stckgen  21869  kgen2ss  21870  kgencn3  21873  ptbasfi  21896  ptpjopn  21927  txdis  21947  txkgen  21967  xkoptsub  21969  xkopjcn  21971  txconn  22004  qtoptop2  22014  qtopuni  22017  qtopkgen  22025  basqtop  22026  tgqtop  22027  qtopss  22030  qtoprest  22032  qtopomap  22033  qtopcmap  22034  kqsat  22046  kqcldsat  22048  hmphdis  22111  isfild  22173  ssfg  22187  fgss  22188  fgss2  22189  fgfil  22190  fgabs  22194  filconn  22198  fgtr  22205  uzrest  22212  ufilmax  22222  ufileu  22234  filufint  22235  rnelfm  22268  fmfnfmlem2  22270  fmfnfmlem4  22272  flimss2  22287  flimss1  22288  flimclsi  22293  flimcf  22297  flimsncls  22301  fclssscls  22333  fclsss1  22337  fclsss2  22338  fclscf  22340  uffclsflim  22346  alexsublem  22359  alexsubALTlem3  22364  ptcmplem2  22368  ptcmplem3  22369  cnextf  22381  symgtgp  22416  cldsubg  22425  tsmscl  22449  haustsms2  22451  tgptsmscls  22464  tsmsxp  22469  restutop  22552  ustuqtop4  22559  utop2nei  22565  utop3cls  22566  ucncn  22600  xblss2ps  22717  xblss2  22718  xrsblre  23125  xrsmopn  23126  recld2  23128  zdis  23130  icccmplem2  23137  cncfss  23213  cnheiborlem  23264  htpycn  23283  phtpyhtpy  23292  pi1blem  23349  cphsscph  23560  cfilfcls  23583  iscmet3lem2  23601  iscmet2  23603  caussi  23606  equivcfil  23608  lmcau  23622  metsscmetcld  23624  hlhil  23752  ivthicc  23765  ovoliunnul  23814  ovolicopnf  23831  uniioombllem3  23892  dyadmbllem  23906  volsup2  23912  vitalilem2  23916  itg1addlem4  24006  itg10a  24017  itg1ge0a  24018  mbfi1fseqlem4  24025  itg2gt0  24067  limciun  24198  perfdvf  24207  cpnord  24238  dvcj  24253  dvlip2  24298  dvivth  24313  dvne0  24314  dvcnvre  24322  ply1lpir  24478  plyco0  24488  plyexmo  24608  abelth  24735  efif1o  24834  logno1  24923  efopnlem2  24944  loglesqrt  25043  lgamcvg2  25337  ppisval  25386  ppinprm  25434  chtnprm  25436  fsumvma  25494  dchrfi  25536  chtppilimlem2  25755  chebbnd2  25758  vmadivsumb  25764  rplogsumlem2  25766  dchrisumlem2  25771  vmalogdivsum2  25819  vmalogdivsum  25820  2vmadivsumlem  25821  selbergb  25830  selberg2b  25833  selberg3lem1  25838  selberg3lem2  25839  selberg3  25840  selberg4lem1  25841  selberg4  25842  pntrlog2bndlem2  25859  pntrlog2bndlem4  25861  uhgredgss  26622  usgruspgrb  26672  uhgrissubgr  26763  uhgrspansubgrlem  26778  uhgrspan1  26791  cusgredg  26912  usgredgsscusgredg  26947  ococss  28854  shsub1  28885  shless  28920  shmodsi  28950  pjhth  28954  spansnss  29132  spanpr  29141  spansnm0i  29211  pjjsi  29261  sumdmdii  29976  sumdmdlem  29979  sumdmdlem2  29980  cdj3lem1  29995  abrexss  30054  fnpreimac  30181  rnmposs  30184  unifi3  30203  uzssico  30262  ssnnssfz  30265  dimkerim  30652  extdg1id  30682  crefss  30757  cmpcref  30758  tpr2rico  30799  esumrnmpt2  30971  esumpcvgval  30981  ldsysgenld  31064  sigapildsys  31066  ldgenpisys  31070  cldssbrsiga  31091  measdivcstOLD  31128  mbfmcnt  31171  oddpwdc  31257  eulerpartlemgs2  31283  reprpmtf1o  31545  bnj1033  31886  bnj1398  31951  sconnpi1  32071  cvmscld  32105  cvmliftlem15  32130  dfon2lem6  32553  fprlem2  32659  fnessref  33226  fgmin  33239  tailfb  33246  dissneqlem  34063  icoreresf  34075  rdglimss  34100  finxpreclem6  34118  lindsenlbs  34328  poimirlem11  34344  poimirlem12  34345  sstotbnd3  34496  prdstotbnd  34514  cntotbnd  34516  ismtyhmeo  34525  1idl  34746  lshpdisj  35568  lssats  35593  lkrin  35745  glbconxN  35959  paddss1  36398  paddss2  36399  paddasslem16  36416  paddidm  36422  pmodlem2  36428  pmapjoin  36433  pmapjat1  36434  pclfinN  36481  pclfinclN  36531  diasslssN  37640  dia2dimlem12  37656  dihsslss  37857  baerlem3lem2  38291  baerlem5alem2  38292  baerlem5blem2  38293  qsalrel  38570  eldiophss  38767  rencldnfilem  38813  pellexlem5  38826  pell14qrss1234  38849  pell1qrss14  38861  pellfundre  38874  pellfundge  38875  pellfundlb  38877  pellfundglb  38878  harinf  39027  proot1hash  39196  intabssd  39332  ss2iundf  39367  ov2ssiunov2  39408  clsk1indlem3  39756  trivsubgd2  40014  trivnsgd  40015  radcnvrat  40062  nznngen  40064  trsspwALT3  40573  sspwimpALT2  40681  refsumcn  40706  iinssf  40830  icoiccdif  41232  icccncfext  41601  stoweidlem27  41744  stoweidlem46  41763  stoweidlem57  41774  fourierdlem40  41864  fourierdlem78  41901  ffnafv  42777  iccpartrn  42963  sprsymrelfvlem  43021  sprsymrelf1lem  43022  rnghmsscmap2  43609  rnghmsscmap  43610  funcrngcsetc  43634  funcrngcsetcALT  43635  rhmsscmap2  43655  rhmsscmap  43656  rhmsscrnghm  43662  rngcresringcat  43666  funcringcsetc  43671  funcringcsetcALTV2lem8  43679  funcringcsetclem8ALTV  43702  rhmsubcALTVlem4  43743  ssnn0ssfz  43762  lincolss  43857  lcoss  43859  lcosslsp  43861  iunord  44147