Theorem ssrdv 3973

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

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

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqelssd  3988  sscon  4115  ssdif  4116  unss1  4155  ssrin  4210  eq0rdv  4357  sspw  4552  elpwdifsn  4721  uniss  4846  intss1  4891  intmin  4896  intssuni  4898  iinssiun  4932  iunss1  4933  iinss1  4934  ss2iun  4937  ssiun  4970  ssiun2  4971  iinss  4980  iinss2  4981  iunxdif3  5017  sspwb  5342  pwssun  5456  relop  5721  dmss  5771  dmcosseq  5844  ssrnres  6035  sossfld  6043  predpo  6166  preddowncl  6175  tron  6214  tz7.7  6217  dffv2  6756  chfnrn  6819  fvn0ssdmfun  6842  fveqdmss  6846  dff3  6866  ffnfv  6882  f1imass  7022  ssorduni  7500  onint  7510  limsssuc  7565  limuni3  7567  limomss  7585  fo1stres  7715  fo2ndres  7716  fo2ndf  7817  fnse  7827  ressuppssdif  7851  suppss  7860  reldmtpos  7900  onfununi  7978  smoiun  7998  smorndom  8005  tz7.48-1  8079  tz7.49  8081  oaass  8187  qsss  8358  uniinqs  8377  pmss12g  8433  mapss  8453  ixpssmap2g  8491  ixpssmapg  8492  fineqv  8733  pssnn  8736  ssfii  8883  dffi2  8887  oismo  9004  unxpwdom2  9052  inf3lemd  9090  inf3lem1  9091  inf3lem6  9096  cantnflem3  9154  cantnf  9156  cnfcom3lem  9166  onssr1  9260  rankunb  9279  tcrank  9313  harcard  9407  carduni  9410  infxpenlem  9439  infpwfien  9488  dfac12r  9572  ackbij2lem1  9641  ackbij1lem18  9659  isfin1-3  9808  fin1a2lem11  9832  fin1a2lem13  9834  zorn2lem4  9921  zorn2lem5  9922  ttukeylem6  9936  ttukeylem7  9937  fpwwe2lem11  10062  fpwwe2lem12  10063  fpwwe2  10065  wunr1om  10141  wunom  10142  tskr1om  10189  tskr1om2  10190  tskxpss  10194  tskcard  10203  tskuni  10205  grothomex  10251  genpss  10426  distrlem1pr  10447  distrlem5pr  10449  ltexprlem2  10459  ltexprlem6  10463  ltexprlem7  10464  reclem3pr  10471  reclem4pr  10472  supaddc  11608  supadd  11609  supmul1  11610  supmullem2  11612  peano5uzi  12072  uzss  12266  ixxdisj  12754  ixxss1  12757  ixxss2  12758  ixxss12  12759  ixxub  12760  ixxlb  12761  iocssre  12817  icossre  12818  iccssre  12819  icodisj  12863  fzss1  12947  fzss2  12948  ssfzunsnext  12953  fzosplit  13071  fzouzsplit  13073  ssfzo12bi  13133  ssnn0fi  13354  fsuppmapnn0fiub  13360  suppssfz  13363  sswrd  13870  rtrclreclem3  14419  isercoll  15024  summolem2a  15072  fsumcvg3  15086  fsum2dlem  15125  fsumcom2  15129  qshash  15182  prodmolem2a  15288  fprod2dlem  15334  fprodcom2  15338  bitsfzo  15784  1arith  16263  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  ramtlecl  16336  prmgaplem3  16389  prmgaplem4  16390  monhom  17005  epihom  17012  funcsetcres2  17353  funcestrcsetclem8  17397  funcsetcestrclem8  17412  psdmrn  17817  gsumwspan  18011  frmdss2  18028  sursubmefmnd  18061  injsubmefmnd  18062  trivsubgsnd  18306  ssnmz  18318  trivnsgd  18324  conjnmz  18392  symgvalstruct  18525  gex1  18716  sylow2alem1  18742  lsmless1x  18769  lsmless2x  18770  lsmub1x  18771  lsmub2x  18772  lsmmod  18801  lsmdisj2  18808  efgrelexlemb  18876  efgcpbllemb  18881  cntzcmn  18960  gsum2d2  19094  dprdub  19147  dprdss  19151  dprddisj2  19161  pgpfac1lem3  19199  kerf1ghm  19497  kerf1hrmOLD  19498  isdrng2  19512  subrguss  19550  subrgmre  19559  primefld0cl  19585  primefld1cl  19586  lssssr  19725  lsssssubg  19730  lssmre  19738  lbspss  19854  lspdisj  19897  lbsextlem2  19931  lidl1el  19991  drngnidl  20002  lpiss  20023  unitrrg  20066  mhpsubg  20340  zsssubrg  20603  qsssubdrg  20604  cnsubrg  20605  mulgrhm2  20646  znrrg  20712  ocvocv  20815  ocv2ss  20817  ocvin  20818  lsmcss  20836  cssmre  20837  pjcss  20860  lindfrn  20965  dmatsgrp  21108  scmatsgrp  21128  scmatsgrp1  21131  m2cpmrngiso  21366  bastg  21574  tgss  21576  tgtop  21581  tgidm  21588  en2top  21593  neisspw  21715  topssnei  21732  neiptopuni  21738  lpss3  21752  clslp  21756  tgrest  21767  ssrest  21784  restntr  21790  ordtbas2  21799  ordtbas  21800  cnss1  21884  cnss2  21885  cnsscnp  21887  cnrest2r  21895  cmpsublem  22007  cmpsub  22008  tgcmp  22009  cmpcld  22010  hauscmplem  22014  cnconn  22030  llyss  22087  nllyss  22088  restnlly  22090  restlly  22091  locfincmp  22134  locfincf  22139  kgenss  22151  kgenidm  22155  llycmpkgen2  22158  1stckgen  22162  kgen2ss  22163  kgencn3  22166  ptbasfi  22189  ptpjopn  22220  txdis  22240  txkgen  22260  xkoptsub  22262  xkopjcn  22264  txconn  22297  qtoptop2  22307  qtopuni  22310  qtopkgen  22318  basqtop  22319  tgqtop  22320  qtopss  22323  qtoprest  22325  qtopomap  22326  qtopcmap  22327  kqsat  22339  kqcldsat  22341  hmphdis  22404  isfild  22466  ssfg  22480  fgss  22481  fgss2  22482  fgfil  22483  fgabs  22487  filconn  22491  fgtr  22498  uzrest  22505  ufilmax  22515  ufileu  22527  filufint  22528  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  flimss2  22580  flimss1  22581  flimclsi  22586  flimcf  22590  flimsncls  22594  fclssscls  22626  fclsss1  22630  fclsss2  22631  fclscf  22633  uffclsflim  22639  alexsublem  22652  alexsubALTlem3  22657  ptcmplem2  22661  ptcmplem3  22662  cnextf  22674  efmndtmd  22709  symgtgp  22714  cldsubg  22719  tsmscl  22743  haustsms2  22745  tgptsmscls  22758  tsmsxp  22763  restutop  22846  ustuqtop4  22853  utop2nei  22859  utop3cls  22860  ucncn  22894  xblss2ps  23011  xblss2  23012  xrsblre  23419  xrsmopn  23420  recld2  23422  zdis  23424  icccmplem2  23431  cncfss  23507  cnheiborlem  23558  htpycn  23577  phtpyhtpy  23586  pi1blem  23643  cphsscph  23854  cfilfcls  23877  iscmet3lem2  23895  iscmet2  23897  caussi  23900  equivcfil  23902  lmcau  23916  metsscmetcld  23918  hlhil  24046  ivthicc  24059  ovoliunnul  24108  ovolicopnf  24125  uniioombllem3  24186  dyadmbllem  24200  volsup2  24206  vitalilem2  24210  itg1addlem4  24300  itg10a  24311  itg1ge0a  24312  mbfi1fseqlem4  24319  itg2gt0  24361  limciun  24492  perfdvf  24501  cpnord  24532  dvcj  24547  dvlip2  24592  dvivth  24607  dvne0  24608  dvcnvre  24616  ply1lpir  24772  plyco0  24782  plyexmo  24902  abelth  25029  efif1o  25130  logno1  25219  efopnlem2  25240  loglesqrt  25339  lgamcvg2  25632  ppisval  25681  ppinprm  25729  chtnprm  25731  fsumvma  25789  dchrfi  25831  chtppilimlem2  26050  chebbnd2  26053  vmadivsumb  26059  rplogsumlem2  26061  dchrisumlem2  26066  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  selbergb  26125  selberg2b  26128  selberg3lem1  26133  selberg3lem2  26134  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  uhgredgss  26916  usgruspgrb  26966  uhgrissubgr  27057  uhgrspansubgrlem  27072  uhgrspan1  27085  cusgredg  27206  usgredgsscusgredg  27241  ococss  29070  shsub1  29101  shless  29136  shmodsi  29166  pjhth  29170  spansnss  29348  spanpr  29357  spansnm0i  29427  pjjsi  29477  sumdmdii  30192  sumdmdlem  30195  sumdmdlem2  30196  cdj3lem1  30211  abrexss  30272  fnpreimac  30416  rnmposs  30419  unifi3  30448  uzssico  30507  ssnnssfz  30510  pmtrcnel  30733  cycpmrn  30785  cyc3evpm  30792  cycpmgcl  30795  dimkerim  31023  extdg1id  31053  crefss  31113  cmpcref  31114  tpr2rico  31155  esumrnmpt2  31327  esumpcvgval  31337  ldsysgenld  31419  sigapildsys  31421  ldgenpisys  31425  cldssbrsiga  31446  measdivcstALTV  31484  mbfmcnt  31526  oddpwdc  31612  eulerpartlemgs2  31638  reprpmtf1o  31897  bnj1033  32241  bnj1398  32306  sconnpi1  32486  cvmscld  32520  cvmliftlem15  32545  satfrnmapom  32617  dfon2lem6  33033  fprlem2  33138  fnessref  33705  fgmin  33718  tailfb  33725  dissneqlem  34624  icoreresf  34636  rdglimss  34661  finxpreclem6  34680  lindsenlbs  34902  poimirlem11  34918  poimirlem12  34919  sstotbnd3  35069  prdstotbnd  35087  cntotbnd  35089  ismtyhmeo  35098  1idl  35319  lshpdisj  36138  lssats  36163  lkrin  36315  glbconxN  36529  paddss1  36968  paddss2  36969  paddasslem16  36986  paddidm  36992  pmodlem2  36998  pmapjoin  37003  pmapjat1  37004  pclfinN  37051  pclfinclN  37101  diasslssN  38210  dia2dimlem12  38226  dihsslss  38427  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  eldiophss  39420  rencldnfilem  39466  pellexlem5  39479  pell14qrss1234  39502  pell1qrss14  39514  pellfundre  39527  pellfundge  39528  pellfundlb  39530  pellfundglb  39531  harinf  39680  proot1hash  39849  intabssd  39934  ss2iundf  40053  ov2ssiunov2  40094  clsk1indlem3  40442  radcnvrat  40695  nznngen  40697  trsspwALT3  41203  sspwimpALT2  41311  refsumcn  41336  iinssf  41456  icoiccdif  41849  icccncfext  42219  stoweidlem27  42361  stoweidlem46  42380  stoweidlem57  42391  fourierdlem40  42481  fourierdlem78  42518  ffnafv  43419  iccpartrn  43639  sprsymrelfvlem  43701  sprsymrelf1lem  43702  rnghmsscmap2  44293  rnghmsscmap  44294  funcrngcsetc  44318  funcrngcsetcALT  44319  rhmsscmap2  44339  rhmsscmap  44340  rhmsscrnghm  44346  rngcresringcat  44350  funcringcsetc  44355  funcringcsetcALTV2lem8  44363  funcringcsetclem8ALTV  44386  rhmsubcALTVlem4  44427  ssnn0ssfz  44446  lincolss  44538  lcoss  44540  lcosslsp  44542  iunord  44828