Theorem ssrdv 3944

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ss 3923

This theorem is used by:  eqelssd  3959  ss2abim  4015  ss2abdv  4020  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  eq0rdvALT  4373  sspw  4575  elpwdifsn  4759  uniss  4882  intss1  4930  intmin  4935  intssuni  4937  iinssiun  4972  iunss1  4973  iinss1  4974  ss2iun  4977  ssiun  5013  ssiun2  5014  iinss  5023  iinss2  5024  iunxdif3  5063  sspwb  5432  pwssun  5555  relop  5838  dmss  5894  dmcosseq  5970  dmcosseqOLD  5971  ssrnres  6178  sossfld  6186  imadifssran  6204  imadifssranOLD  6205  predtrss  6327  preddowncl  6337  tron  6387  tz7.7  6390  funimassd  6951  dffv2  6980  chfnrn  7048  fvn0ssdmfun  7073  fveqdmss  7077  dff3  7099  ffnfv  7118  f1imass  7267  ssorduni  7784  onint  7795  limsssuc  7852  limuni3  7854  limomss  7873  fo1stres  8018  fo2ndres  8019  fo2ndf  8122  fnse  8135  ressuppssdif  8187  suppss  8196  reldmtpos  8236  fprlem2  8304  onfununi  8334  smoiun  8354  smocdmdom  8361  tz7.48-1  8436  tz7.49  8438  oaass  8552  cofon1  8664  cofon2  8665  qsss  8779  uniinqs  8801  pmss12g  8873  mapss  8893  ixpssmap2g  8931  ixpssmapg  8932  pssnn  9160  fineqv  9234  unifi3  9326  finnzfsuppd  9340  ssfii  9386  dffi2  9390  oismo  9509  unxpwdom2  9557  inf3lemd  9603  inf3lem1  9604  inf3lem6  9609  cantnflem3  9667  cantnf  9669  cnfcom3lem  9679  onssr1  9810  rankunb  9829  tcrank  9863  harcard  9980  carduni  9983  infxpenlem  10013  infpwfien  10062  dfac12r  10146  ackbij2lem1  10217  ackbij1lem18  10235  isfin1-3  10385  fin1a2lem11  10409  fin1a2lem13  10411  zorn2lem4  10498  zorn2lem5  10499  ttukeylem6  10513  ttukeylem7  10514  fpwwe2lem10  10640  fpwwe2lem11  10641  fpwwe2  10643  wunr1om  10719  wunom  10720  tskr1om  10767  tskr1om2  10768  tskxpss  10772  tskcard  10781  tskuni  10783  grothomex  10829  genpss  11004  distrlem1pr  11025  distrlem5pr  11027  ltexprlem2  11037  ltexprlem6  11041  ltexprlem7  11042  reclem3pr  11049  reclem4pr  11050  supaddc  12197  supadd  12198  supmul1  12199  supmullem2  12201  peano5uzi  12701  uzss  12901  ixxdisj  13403  ixxss1  13406  ixxss2  13407  ixxss12  13408  ixxub  13409  ixxlb  13410  iocssre  13470  icossre  13471  iccssre  13472  icodisj  13519  fzss1  13608  fzss2  13609  ssfzunsnext  13614  fzosplit  13738  fzouzsplit  13740  ssfzo12bi  13807  ssnn0fi  14039  fsuppmapnn0fiub  14045  suppssfz  14048  sswrd  14577  rtrclreclem3  15121  isercoll  15743  summolem2a  15789  fsumcvg3  15803  fsum2dlem  15844  fsumcom2  15848  qshash  15902  prodmolem2a  16011  fprod2dlem  16057  fprodcom2  16061  bitsfzo  16515  1arith  17009  vdwlem2  17064  vdwlem6  17068  vdwlem8  17070  ramtlecl  17082  prmgaplem3  17135  prmgaplem4  17136  monhom  17814  epihom  17821  funcsetcres2  18172  funcestrcsetclem8  18225  funcsetcestrclem8  18240  psdmrn  18651  chnrss  18693  chndss  18694  gsumwspan  18942  frmdss2  18959  sursubmefmnd  18992  injsubmefmnd  18993  trivsubgsnd  19264  ssnmz  19276  trivnsgd  19282  kerf1ghm  19361  conjnmz  19366  symgvalstruct  19511  gex1  19705  sylow2alem1  19731  lsmless1x  19758  lsmless2x  19759  lsmub1x  19760  lsmub2x  19761  lsmmod  19789  lsmdisj2  19796  efgrelexlemb  19864  efgcpbllemb  19869  cntzcmn  19954  gsum2d2  20088  dprdub  20141  dprdss  20145  dprddisj2  20155  pgpfac1lem3  20193  subrngmre  20711  subrguss  20736  subrgmre  20746  rnghmsscmap2  20778  rnghmsscmap  20779  funcrngcsetc  20789  funcrngcsetcALT  20790  rhmsscmap2  20807  rhmsscmap  20808  rhmsscrnghm  20814  rngcresringcat  20818  funcringcsetc  20823  unitrrg  20852  isdrng2  20893  primefld0cl  20959  primefld1cl  20960  lssssr  21125  lsssssubg  21129  lssmre  21137  lbspss  21253  lspdisj  21299  lbsextlem2  21333  lidl1el  21401  drngnidl  21427  prmidlssidl  21520  lpiss  21547  zsssubrg  21625  qsssubdrg  21626  cnsubrg  21627  mulgrhm2  21678  znrrg  21765  ocvocv  21871  ocv2ss  21873  ocvin  21874  lsmcss  21892  cssmre  21893  pjcss  21916  lindfrn  22021  sraassab  22068  mhpsubg  22366  evls1maprnss  22588  dmatsgrp  22706  scmatsgrp  22726  scmatsgrp1  22729  m2cpmrngiso  22965  bastg  23173  tgss  23175  tgtop  23180  tgidm  23187  en2top  23192  neisspw  23314  topssnei  23331  neiptopuni  23337  lpss3  23351  clslp  23355  tgrest  23366  ssrest  23383  restntr  23389  ordtbas2  23398  ordtbas  23399  cnss1  23483  cnss2  23484  cnsscnp  23486  cnrest2r  23494  cmpsublem  23606  cmpsub  23607  tgcmp  23608  cmpcld  23609  hauscmplem  23613  cnconn  23629  llyss  23687  nllyss  23688  restnlly  23690  restlly  23691  locfincmp  23734  locfincf  23739  kgenss  23751  kgenidm  23755  llycmpkgen2  23758  1stckgen  23762  kgen2ss  23763  kgencn3  23766  ptbasfi  23789  ptpjopn  23820  txdis  23840  txkgen  23860  xkoptsub  23862  xkopjcn  23864  txconn  23897  qtoptop2  23907  qtopuni  23910  qtopkgen  23918  basqtop  23919  tgqtop  23920  qtopss  23923  qtoprest  23925  qtopomap  23926  qtopcmap  23927  kqsat  23939  kqcldsat  23941  hmphdis  24004  isfild  24066  ssfg  24080  fgss  24081  fgss2  24082  fgfil  24083  fgabs  24087  filconn  24091  fgtr  24098  uzrest  24105  ufilmax  24115  ufileu  24127  filufint  24128  rnelfm  24161  fmfnfmlem2  24163  fmfnfmlem4  24165  flimss2  24180  flimss1  24181  flimclsi  24186  flimcf  24190  flimsncls  24194  fclssscls  24226  fclsss1  24230  fclsss2  24231  fclscf  24233  uffclsflim  24239  alexsublem  24252  alexsubALTlem3  24257  ptcmplem2  24261  ptcmplem3  24262  cnextf  24274  efmndtmd  24309  symgtgp  24314  cldsubg  24319  tsmscl  24343  haustsms2  24345  tgptsmscls  24358  tsmsxp  24363  restutop  24445  ustuqtop4  24452  utop2nei  24458  utop3cls  24459  ucncn  24492  xblss2ps  24609  xblss2  24610  xrsblre  25020  xrsmopn  25021  recld2  25023  zdis  25025  icccmplem2  25032  cncfss  25109  cnheiborlem  25164  htpycn  25183  phtpyhtpy  25192  pi1blem  25249  cphsscph  25461  cfilfcls  25484  iscmet3lem2  25502  iscmet2  25504  caussi  25507  equivcfil  25509  lmcau  25523  metsscmetcld  25525  hlhil  25653  ivthicc  25668  ovoliunnul  25717  ovolicopnf  25734  uniioombllem3  25795  dyadmbllem  25809  volsup2  25815  vitalilem2  25819  itg1addlem4  25909  itg10a  25920  itg1ge0a  25921  mbfi1fseqlem4  25928  itg2gt0  25970  limciun  26104  perfdvf  26113  cpnord  26145  dvcj  26160  dvlip2  26205  dvivth  26220  dvne0  26221  dvcnvre  26229  ply1lpir  26390  plyco0  26400  plyexmo  26525  abelth  26655  efif1o  26762  logno1  26852  efopnlem2  26873  loglesqrt  26977  lgamcvg2  27270  ppisval  27319  ppinprm  27367  chtnprm  27369  fsumvma  27428  dchrfi  27470  chtppilimlem2  27689  chebbnd2  27692  vmadivsumb  27698  rplogsumlem2  27700  dchrisumlem2  27705  vmalogdivsum2  27753  vmalogdivsum  27754  2vmadivsumlem  27755  selbergb  27764  selberg2b  27767  selberg3lem1  27772  selberg3lem2  27773  selberg3  27774  selberg4lem1  27775  selberg4  27776  pntrlog2bndlem2  27793  pntrlog2bndlem4  27795  oldssmade  28111  ltslpss  28152  noseqrdgfn  28550  n0ssoldg  28597  peano5uzs  28648  elplnglnid  29116  lnincplng  29117  plngrotlem2  29121  prlngpln3  29254  uhgredgss  29536  usgruspgrb  29591  uhgrissubgr  29683  uhgrspansubgrlem  29698  uhgrspan1  29711  cusgredg  29832  usgredgsscusgredg  29867  ococss  31716  shsub1  31747  shless  31782  shmodsi  31812  pjhth  31816  spansnss  31994  spanpr  32003  spansnm0i  32073  pjjsi  32123  sumdmdii  32838  sumdmdlem  32841  sumdmdlem2  32842  cdj3lem1  32857  abrexss  32929  fnpreimac  33086  rnmposs  33089  uzssico  33199  ssnnssfz  33202  pwrssmgc  33384  pmtrcnel  33473  cycpmrn  33527  cyc3evpm  33534  cycpmgcl  33537  elrgspnlem1  33626  elrgspnlem3  33628  elrgspnlem4  33629  elrgspnsubrunlem2  33632  fldgensdrg  33699  ringlsmss1  33771  ringlsmss2  33772  mxidlirredi  33818  drngmxidl  33823  drngmxidlr  33824  1arithidomlem1  33889  1arithidom  33891  1arithufdlem2  33899  1arithufdlem3  33900  1arithufdlem4  33901  dfufd2lem  33903  ply1mulrtss  33936  esplyfvaln  34028  dimkerim  34081  extdg1id  34120  irngss  34141  irngssv  34142  algextdeglem8  34178  constrsscn  34194  constrsslem  34195  constrsdrg  34229  crefss  34303  cmpcref  34304  zarmxt1  34334  tpr2rico  34366  esumrnmpt2  34522  esumpcvgval  34532  ldsysgenld  34615  sigapildsys  34617  ldgenpisys  34621  cldssbrsiga  34642  measdivcstALTV  34680  mbfmcnt  34723  oddpwdc  34809  eulerpartlemgs2  34835  reprpmtf1o  35078  bnj1033  35422  bnj1398  35487  trssfir1om  35565  r1omhfb  35566  trssfir1omregs  35606  r1omhfbregs  35607  sconnpi1  35768  cvmscld  35802  cvmliftlem15  35827  satfrnmapom  35899  dfon2lem6  36315  fnessref  36925  fgmin  36938  tailfb  36945  dissneqlem  38043  icoreresf  38055  rdglimss  38080  finxpreclem6  38099  lindsenlbs  38323  poimirlem11  38339  poimirlem12  38340  sstotbnd3  38485  prdstotbnd  38503  cntotbnd  38505  ismtyhmeo  38514  1idl  38735  disjdmqsss  39612  lshpdisj  39819  lssats  39844  lkrin  39996  glbconxN  40210  paddss1  40649  paddss2  40650  paddasslem16  40667  paddidm  40673  pmodlem2  40679  pmapjoin  40684  pmapjat1  40685  pclfinN  40732  pclfinclN  40782  diasslssN  41891  dia2dimlem12  41907  dihsslss  42108  baerlem3lem2  42542  baerlem5alem2  42543  baerlem5blem2  42544  zndvdchrrhm  42798  dvrelog2  42889  dvrelog3  42890  aks4d1p3  42903  aks4d1p4  42904  aks4d1p5  42905  aks4d1p7  42908  aks4d1p8  42912  primrootsunit1  42922  primrootscoprmpow  42924  primrootscoprbij  42927  hashscontpow1  42946  aks6d1c4  42949  sticksstones3  42973  aks6d1c6lem3  42997  aks6d1c6isolem2  43000  aks6d1c6lem5  43002  rhmqusspan  43010  unitscyglem1  43020  unitscyglem4  43023  eldiophss  43563  rencldnfilem  43605  pellexlem5  43618  pell14qrss1234  43641  pell1qrss14  43653  pellfundre  43666  pellfundge  43667  pellfundlb  43669  pellfundglb  43670  harinf  43819  proot1hash  43980  safesnsupfiss  44199  intabssd  44303  ss2iundf  44443  ov2ssiunov2  44484  clsk1indlem3  44827  radcnvrat  45082  nznngen  45084  trsspwALT3  45586  sspwimpALT2  45694  refsumcn  45808  iinssf  45914  icoiccdif  46298  icccncfext  46659  stoweidlem27  46799  stoweidlem46  46818  stoweidlem57  46829  fourierdlem40  46919  fourierdlem78  46956  ffnafv  47966  iccpartrn  48237  sprsymrelfvlem  48297  sprsymrelf1lem  48298  clnbgrssedg  48664  stgrusgra  48782  rhmsubcALTVlem4  49106  funcringcsetcALTV2lem8  49119  funcringcsetclem8ALTV  49142  ssnn0ssfz  49186  lincolss  49271  lcoss  49273  lcosslsp  49275  iunord  50511