Theorem ssrdv 3921

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

Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqelssd  3936  ss2abdvALT  3992  sscon  4066  ssdif  4067  unss1  4106  ssrin  4160  eq0rdv  4312  sspw  4510  elpwdifsn  4682  uniss  4808  intss1  4853  intmin  4858  intssuni  4860  iinssiun  4894  iunss1  4895  iinss1  4896  ss2iun  4899  ssiun  4933  ssiun2  4934  iinss  4943  iinss2  4944  iunxdif3  4980  sspwb  5307  pwssun  5421  relop  5685  dmss  5735  dmcosseq  5809  ssrnres  6002  sossfld  6010  predpo  6134  preddowncl  6143  tron  6182  tz7.7  6185  dffv2  6733  chfnrn  6796  fvn0ssdmfun  6819  fveqdmss  6823  dff3  6843  ffnfv  6859  f1imass  7000  ssorduni  7480  onint  7490  limsssuc  7545  limuni3  7547  limomss  7565  fo1stres  7697  fo2ndres  7698  fo2ndf  7800  fnse  7810  ressuppssdif  7834  suppss  7843  reldmtpos  7883  onfununi  7961  smoiun  7981  smorndom  7988  tz7.48-1  8062  tz7.49  8064  oaass  8170  qsss  8341  uniinqs  8360  pmss12g  8416  mapss  8436  ixpssmap2g  8474  ixpssmapg  8475  fineqv  8717  pssnn  8720  ssfii  8867  dffi2  8871  oismo  8988  unxpwdom2  9036  inf3lemd  9074  inf3lem1  9075  inf3lem6  9080  cantnflem3  9138  cantnf  9140  cnfcom3lem  9150  onssr1  9244  rankunb  9263  tcrank  9297  harcard  9391  carduni  9394  infxpenlem  9424  infpwfien  9473  dfac12r  9557  ackbij2lem1  9630  ackbij1lem18  9648  isfin1-3  9797  fin1a2lem11  9821  fin1a2lem13  9823  zorn2lem4  9910  zorn2lem5  9911  ttukeylem6  9925  ttukeylem7  9926  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2  10054  wunr1om  10130  wunom  10131  tskr1om  10178  tskr1om2  10179  tskxpss  10183  tskcard  10192  tskuni  10194  grothomex  10240  genpss  10415  distrlem1pr  10436  distrlem5pr  10438  ltexprlem2  10448  ltexprlem6  10452  ltexprlem7  10453  reclem3pr  10460  reclem4pr  10461  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  peano5uzi  12059  uzss  12253  ixxdisj  12741  ixxss1  12744  ixxss2  12745  ixxss12  12746  ixxub  12747  ixxlb  12748  iocssre  12805  icossre  12806  iccssre  12807  icodisj  12854  fzss1  12941  fzss2  12942  ssfzunsnext  12947  fzosplit  13065  fzouzsplit  13067  ssfzo12bi  13127  ssnn0fi  13348  fsuppmapnn0fiub  13354  suppssfz  13357  sswrd  13865  rtrclreclem3  14411  isercoll  15016  summolem2a  15064  fsumcvg3  15078  fsum2dlem  15117  fsumcom2  15121  qshash  15174  prodmolem2a  15280  fprod2dlem  15326  fprodcom2  15330  bitsfzo  15774  1arith  16253  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  ramtlecl  16326  prmgaplem3  16379  prmgaplem4  16380  monhom  16997  epihom  17004  funcsetcres2  17345  funcestrcsetclem8  17389  funcsetcestrclem8  17404  psdmrn  17809  gsumwspan  18003  frmdss2  18020  sursubmefmnd  18053  injsubmefmnd  18054  trivsubgsnd  18298  ssnmz  18310  trivnsgd  18316  conjnmz  18384  symgvalstruct  18517  gex1  18708  sylow2alem1  18734  lsmless1x  18761  lsmless2x  18762  lsmub1x  18763  lsmub2x  18764  lsmmod  18793  lsmdisj2  18800  efgrelexlemb  18868  efgcpbllemb  18873  cntzcmn  18953  gsum2d2  19087  dprdub  19140  dprdss  19144  dprddisj2  19154  pgpfac1lem3  19192  kerf1ghm  19491  isdrng2  19505  subrguss  19543  subrgmre  19552  primefld0cl  19578  primefld1cl  19579  lssssr  19718  lsssssubg  19723  lssmre  19731  lbspss  19847  lspdisj  19890  lbsextlem2  19924  lidl1el  19984  drngnidl  19995  lpiss  20016  unitrrg  20059  zsssubrg  20149  qsssubdrg  20150  cnsubrg  20151  mulgrhm2  20192  znrrg  20257  ocvocv  20360  ocv2ss  20362  ocvin  20363  lsmcss  20381  cssmre  20382  pjcss  20405  lindfrn  20510  mhpvarcl  20798  mhpsubg  20801  dmatsgrp  21104  scmatsgrp  21124  scmatsgrp1  21127  m2cpmrngiso  21363  bastg  21571  tgss  21573  tgtop  21578  tgidm  21585  en2top  21590  neisspw  21712  topssnei  21729  neiptopuni  21735  lpss3  21749  clslp  21753  tgrest  21764  ssrest  21781  restntr  21787  ordtbas2  21796  ordtbas  21797  cnss1  21881  cnss2  21882  cnsscnp  21884  cnrest2r  21892  cmpsublem  22004  cmpsub  22005  tgcmp  22006  cmpcld  22007  hauscmplem  22011  cnconn  22027  llyss  22084  nllyss  22085  restnlly  22087  restlly  22088  locfincmp  22131  locfincf  22136  kgenss  22148  kgenidm  22152  llycmpkgen2  22155  1stckgen  22159  kgen2ss  22160  kgencn3  22163  ptbasfi  22186  ptpjopn  22217  txdis  22237  txkgen  22257  xkoptsub  22259  xkopjcn  22261  txconn  22294  qtoptop2  22304  qtopuni  22307  qtopkgen  22315  basqtop  22316  tgqtop  22317  qtopss  22320  qtoprest  22322  qtopomap  22323  qtopcmap  22324  kqsat  22336  kqcldsat  22338  hmphdis  22401  isfild  22463  ssfg  22477  fgss  22478  fgss2  22479  fgfil  22480  fgabs  22484  filconn  22488  fgtr  22495  uzrest  22502  ufilmax  22512  ufileu  22524  filufint  22525  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  flimss2  22577  flimss1  22578  flimclsi  22583  flimcf  22587  flimsncls  22591  fclssscls  22623  fclsss1  22627  fclsss2  22628  fclscf  22630  uffclsflim  22636  alexsublem  22649  alexsubALTlem3  22654  ptcmplem2  22658  ptcmplem3  22659  cnextf  22671  efmndtmd  22706  symgtgp  22711  cldsubg  22716  tsmscl  22740  haustsms2  22742  tgptsmscls  22755  tsmsxp  22760  restutop  22843  ustuqtop4  22850  utop2nei  22856  utop3cls  22857  ucncn  22891  xblss2ps  23008  xblss2  23009  xrsblre  23416  xrsmopn  23417  recld2  23419  zdis  23421  icccmplem2  23428  cncfss  23504  cnheiborlem  23559  htpycn  23578  phtpyhtpy  23587  pi1blem  23644  cphsscph  23855  cfilfcls  23878  iscmet3lem2  23896  iscmet2  23898  caussi  23901  equivcfil  23903  lmcau  23917  metsscmetcld  23919  hlhil  24047  ivthicc  24062  ovoliunnul  24111  ovolicopnf  24128  uniioombllem3  24189  dyadmbllem  24203  volsup2  24209  vitalilem2  24213  itg1addlem4  24303  itg10a  24314  itg1ge0a  24315  mbfi1fseqlem4  24322  itg2gt0  24364  limciun  24497  perfdvf  24506  cpnord  24538  dvcj  24553  dvlip2  24598  dvivth  24613  dvne0  24614  dvcnvre  24622  ply1lpir  24779  plyco0  24789  plyexmo  24909  abelth  25036  efif1o  25138  logno1  25227  efopnlem2  25248  loglesqrt  25347  lgamcvg2  25640  ppisval  25689  ppinprm  25737  chtnprm  25739  fsumvma  25797  dchrfi  25839  chtppilimlem2  26058  chebbnd2  26061  vmadivsumb  26067  rplogsumlem2  26069  dchrisumlem2  26074  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  selbergb  26133  selberg2b  26136  selberg3lem1  26141  selberg3lem2  26142  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  uhgredgss  26924  usgruspgrb  26974  uhgrissubgr  27065  uhgrspansubgrlem  27080  uhgrspan1  27093  cusgredg  27214  usgredgsscusgredg  27249  ococss  29076  shsub1  29107  shless  29142  shmodsi  29172  pjhth  29176  spansnss  29354  spanpr  29363  spansnm0i  29433  pjjsi  29483  sumdmdii  30198  sumdmdlem  30201  sumdmdlem2  30202  cdj3lem1  30217  abrexss  30280  fnpreimac  30434  rnmposs  30437  unifi3  30474  uzssico  30533  ssnnssfz  30536  pwrssmgc  30706  pmtrcnel  30783  cycpmrn  30835  cyc3evpm  30842  cycpmgcl  30845  ringlsmss1  31003  ringlsmss2  31004  prmidlssidl  31028  dimkerim  31111  extdg1id  31141  crefss  31202  cmpcref  31203  zarmxt1  31233  tpr2rico  31265  esumrnmpt2  31437  esumpcvgval  31447  ldsysgenld  31529  sigapildsys  31531  ldgenpisys  31535  cldssbrsiga  31556  measdivcstALTV  31594  mbfmcnt  31636  oddpwdc  31722  eulerpartlemgs2  31748  reprpmtf1o  32007  bnj1033  32351  bnj1398  32416  sconnpi1  32599  cvmscld  32633  cvmliftlem15  32658  satfrnmapom  32730  dfon2lem6  33146  fprlem2  33251  fnessref  33818  fgmin  33831  tailfb  33838  dissneqlem  34757  icoreresf  34769  rdglimss  34794  finxpreclem6  34813  lindsenlbs  35052  poimirlem11  35068  poimirlem12  35069  sstotbnd3  35214  prdstotbnd  35232  cntotbnd  35234  ismtyhmeo  35243  1idl  35464  lshpdisj  36283  lssats  36308  lkrin  36460  glbconxN  36674  paddss1  37113  paddss2  37114  paddasslem16  37131  paddidm  37137  pmodlem2  37143  pmapjoin  37148  pmapjat1  37149  pclfinN  37196  pclfinclN  37246  diasslssN  38355  dia2dimlem12  38371  dihsslss  38572  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  eldiophss  39715  rencldnfilem  39761  pellexlem5  39774  pell14qrss1234  39797  pell1qrss14  39809  pellfundre  39822  pellfundge  39823  pellfundlb  39825  pellfundglb  39826  harinf  39975  proot1hash  40144  intabssd  40227  ss2iundf  40360  ov2ssiunov2  40401  clsk1indlem3  40746  finnzfsuppd  40915  radcnvrat  41018  nznngen  41020  trsspwALT3  41526  sspwimpALT2  41634  refsumcn  41659  iinssf  41775  icoiccdif  42161  icccncfext  42529  stoweidlem27  42669  stoweidlem46  42688  stoweidlem57  42699  fourierdlem40  42789  fourierdlem78  42826  ffnafv  43727  iccpartrn  43947  sprsymrelfvlem  44007  sprsymrelf1lem  44008  rnghmsscmap2  44597  rnghmsscmap  44598  funcrngcsetc  44622  funcrngcsetcALT  44623  rhmsscmap2  44643  rhmsscmap  44644  rhmsscrnghm  44650  rngcresringcat  44654  funcringcsetc  44659  funcringcsetcALTV2lem8  44667  funcringcsetclem8ALTV  44690  rhmsubcALTVlem4  44731  ssnn0ssfz  44751  lincolss  44843  lcoss  44845  lcosslsp  44847  iunord  45206