Theorem ssrdv 3609

Description: Deduction rule 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 1855	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3591	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 224	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1481   ∈ wcel 1990   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sscon  3744  ssdif  3745  unss1  3782  ssrin  3838  eq0rdv  3979  elpwdifsn  4319  uniss  4458  intss1  4492  intmin  4497  intssuni  4499  iunss1  4532  iinss1  4533  ss2iun  4536  ssiun  4562  ssiun2  4563  iinss  4571  iinss2  4572  iunxdif3  4606  trintssOLD  4770  sspwb  4917  pwssun  5020  relop  5272  dmss  5323  dmcosseq  5387  ssrnres  5572  sossfld  5580  predpo  5698  preddowncl  5707  tron  5746  tz7.7  5749  dffv2  6271  chfnrn  6328  fvn0ssdmfun  6350  fveqdmss  6354  dff3  6372  ffnfv  6388  f1imass  6521  ssorduni  6985  onint  6995  limsssuc  7050  limuni3  7052  limomss  7070  fo1stres  7192  fo2ndres  7193  fo2ndf  7284  fnse  7294  ressuppssdif  7316  suppss  7325  reldmtpos  7360  wfrlem10  7424  onfununi  7438  smoiun  7458  smorndom  7465  tz7.48-1  7538  tz7.49  7540  oaass  7641  qsss  7808  uniinqs  7827  pmss12g  7884  mapss  7900  ixpssmap2g  7937  ixpssmapg  7938  fineqv  8175  pssnn  8178  ssfii  8325  dffi2  8329  ordtypelem9  8431  ordtypelem10  8432  oismo  8445  unxpwdom2  8493  inf3lemd  8524  inf3lem1  8525  inf3lem6  8530  cantnflem3  8588  cantnf  8590  cnfcom3lem  8600  onssr1  8694  rankunb  8713  tcrank  8747  harcard  8804  carduni  8807  infxpenlem  8836  infpwfien  8885  dfac12r  8968  ackbij2lem1  9041  ackbij1lem18  9059  isfin1-3  9208  fin1a2lem11  9232  fin1a2lem13  9234  zorn2lem4  9321  zorn2lem5  9322  ttukeylem6  9336  ttukeylem7  9337  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2  9465  wunr1om  9541  wunom  9542  tskr1om  9589  tskr1om2  9590  tskxpss  9594  tskcard  9603  tskuni  9605  grothomex  9651  genpss  9826  distrlem1pr  9847  distrlem5pr  9849  prlem934  9855  ltexprlem2  9859  ltexprlem6  9863  ltexprlem7  9864  reclem3pr  9871  reclem4pr  9872  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  peano5uzi  11466  uzss  11708  ixxdisj  12190  ixxss1  12193  ixxss2  12194  ixxss12  12195  ixxub  12196  ixxlb  12197  iocssre  12253  icossre  12254  iccssre  12255  icodisj  12297  fzss1  12380  fzss2  12381  ssfzunsnext  12386  fzosplit  12501  fzouzsplit  12503  ssfzo12bi  12563  ssnn0fi  12784  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  suppssfz  12794  sswrd  13313  rtrclreclem3  13800  isercoll  14398  summolem2a  14446  fsumcvg3  14460  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  qshash  14559  prodmolem2a  14664  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  bitsfzo  15157  phimullem  15484  prmreclem5  15624  1arith  15631  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  ramtlecl  15704  prmgaplem3  15757  prmgaplem4  15758  monhom  16395  epihom  16402  funcsetcres2  16743  funcestrcsetclem8  16787  funcsetcestrclem8  16802  psdmrn  17207  psssdm2  17215  gsumwspan  17383  frmdss2  17400  ssnmz  17636  conjnmz  17694  gex1  18006  sylow2alem1  18032  sylow3lem3  18044  lsmless1x  18059  lsmless2x  18060  lsmub1x  18061  lsmub2x  18062  lsmmod  18088  lsmdisj2  18095  efgrelexlemb  18163  efgcpbllemb  18168  cntzcmn  18245  gsum2d2  18373  dprdub  18424  dprdss  18428  dprddisj2  18438  ablfacrp  18465  pgpfac1lem3  18476  kerf1hrm  18743  isdrng2  18757  subrguss  18795  subrgmre  18804  lssssr  18953  lsssssubg  18958  lssmre  18966  lbspss  19082  lspdisj  19125  lbsextlem2  19159  lidl1el  19218  drngnidl  19229  lpiss  19250  unitrrg  19293  fidomndrng  19307  mplbas2  19470  zsssubrg  19804  qsssubdrg  19805  cnsubrg  19806  mulgrhm2  19847  znrrg  19914  ocvocv  20015  ocv2ss  20017  ocvin  20018  lsmcss  20036  cssmre  20037  pjfo  20059  pjcss  20060  obs2ss  20073  frlmsslsp  20135  lindfrn  20160  dmatsgrp  20305  scmatsgrp  20325  scmatsgrp1  20328  m2cpmrngiso  20563  bastg  20770  tgss  20772  tgtop  20777  tgidm  20784  en2top  20789  neisspw  20911  topssnei  20928  neiptopuni  20934  lpss3  20948  clslp  20952  tgrest  20963  ssrest  20980  restfpw  20983  restntr  20986  ordtbas2  20995  ordtbas  20996  cnss1  21080  cnss2  21081  cnsscnp  21083  cnrest2r  21091  cmpsublem  21202  cmpsub  21203  tgcmp  21204  cmpcld  21205  hauscmplem  21209  cnconn  21225  2ndcsep  21262  llyss  21282  nllyss  21283  restnlly  21285  restlly  21286  locfincmp  21329  locfincf  21334  kgenss  21346  kgenidm  21350  llycmpkgen2  21353  1stckgen  21357  kgen2ss  21358  kgencn3  21361  ptbasfi  21384  ptpjopn  21415  ptclsg  21418  txdis  21435  txkgen  21455  xkoptsub  21457  xkopjcn  21459  txconn  21492  qtoptop2  21502  qtopuni  21505  qtopkgen  21513  basqtop  21514  tgqtop  21515  qtopss  21518  qtoprest  21520  qtopomap  21521  qtopcmap  21522  kqsat  21534  kqcldsat  21536  hmphdis  21599  isfild  21662  ssfg  21676  fgss  21677  fgss2  21678  fgfil  21679  fgabs  21683  filconn  21687  fgtr  21694  trfg  21695  uzrest  21701  ufilmax  21711  ufileu  21723  filufint  21724  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  flimss2  21776  flimss1  21777  flimclsi  21782  flimcf  21786  flimsncls  21790  fclssscls  21822  fclsss1  21826  fclsss2  21827  fclscf  21829  uffclsflim  21835  alexsublem  21848  alexsubALTlem3  21853  ptcmplem2  21857  ptcmplem3  21858  cnextf  21870  symgtgp  21905  cldsubg  21914  tsmscl  21938  haustsms2  21940  tgptsmscls  21953  tsmsxp  21958  restutop  22041  restutopopn  22042  ustuqtop4  22048  utop2nei  22054  utop3cls  22055  ucncn  22089  xblss2ps  22206  xblss2  22207  unirnblps  22224  unirnbl  22225  xrsblre  22614  xrsmopn  22615  recld2  22617  zdis  22619  icccmplem2  22626  cncfss  22702  cnheiborlem  22753  htpycn  22772  phtpyhtpy  22781  pi1blem  22839  clsocv  23049  cfilfcls  23072  iscmet3lem2  23090  iscmet2  23092  caussi  23095  equivcfil  23097  lmcau  23111  cmetss  23113  pjth  23210  hlhil  23214  ivthicc  23227  ovoliunnul  23275  ovolicopnf  23292  uniioombllem3  23353  dyadmbllem  23367  opnmbllem  23369  volsup2  23373  vitalilem2  23378  itg1addlem4  23466  itg10a  23477  itg1ge0a  23478  mbfi1fseqlem4  23485  itg2gt0  23527  limciun  23658  perfdvf  23667  dvidlem  23679  cpnord  23698  dvaddf  23705  dvmulf  23706  dvcof  23711  dvcj  23713  dvrec  23718  dvcnv  23740  dvlip2  23758  dvivth  23773  dvne0  23774  dvcnvre  23782  ftc1cn  23806  ply1lpir  23938  plyco0  23948  plyexmo  24068  ulmdv  24157  pserdv  24183  abelth  24195  efif1o  24292  logno1  24382  efopnlem2  24403  loglesqrt  24499  lgamcvg2  24781  ppisval  24830  ppisval2  24831  ppinprm  24878  chtnprm  24880  fsumvma  24938  dchrfi  24980  chtppilimlem2  25163  chebbnd2  25166  vmadivsumb  25172  rplogsumlem2  25174  dchrisumlem2  25179  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  selbergb  25238  selberg2b  25241  selberg3lem1  25246  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  uhgredgss  26026  usgruspgrb  26076  uhgrissubgr  26167  uhgrspansubgrlem  26182  uhgrspan1  26195  nbgrssvtx  26256  nbgrssovtx  26260  cusgredg  26320  usgredgsscusgredg  26355  ococss  28152  shsub1  28183  shless  28218  shmodsi  28248  pjhth  28252  spansnss  28430  spanpr  28439  spansnm0i  28509  pjjsi  28559  sumdmdii  29274  sumdmdlem  29277  sumdmdlem2  29278  cdj3lem1  29293  abrexss  29350  iinssiun  29377  rnmpt2ss  29473  unifi3  29490  uzssico  29546  ssnnssfz  29549  reff  29906  crefss  29916  cmpcref  29917  tpr2rico  29958  esumrnmpt2  30130  esumpcvgval  30140  ldsysgenld  30223  sigapildsys  30225  ldgenpisys  30229  cldssbrsiga  30250  measdivcstOLD  30287  mbfmcnt  30330  dya2iocuni  30345  oddpwdc  30416  eulerpartlemgs2  30442  reprpmtf1o  30704  bnj1033  31037  bnj1398  31102  sconnpi1  31221  cvmscld  31255  cvmsss2  31256  cvmliftlem15  31280  dfon2lem6  31693  fnessref  32352  fgmin  32365  tailfb  32372  dissneqlem  33187  icoreresf  33200  finxpreclem6  33233  lindsenlbs  33404  poimirlem11  33420  poimirlem12  33421  opnmbllem0  33445  ftc1cnnc  33484  sstotbnd3  33575  prdstotbnd  33593  cntotbnd  33595  ismtyhmeo  33604  1idl  33825  lshpdisj  34274  lssats  34299  lkrlsp  34389  lkrin  34451  glbconxN  34664  paddss1  35103  paddss2  35104  paddasslem16  35121  paddidm  35127  pmodlem2  35133  pmapjoin  35138  pmapjat1  35139  pclfinN  35186  pclfinclN  35236  cdleme50rnlem  35832  diasslssN  36348  dia2dimlem12  36364  dihsslss  36565  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmaprnN  37156  hgmaprnN  37193  eldiophss  37338  rencldnfilem  37384  pellexlem5  37397  pell14qrss1234  37420  pell1qrss14  37432  pellfundre  37445  pellfundge  37446  pellfundlb  37448  pellfundglb  37449  harinf  37601  kercvrlsm  37653  pwssplit4  37659  hbtlem5  37698  proot1hash  37778  intabssd  37916  ss2iundf  37951  ov2ssiunov2  37992  clsk1indlem3  38341  radcnvrat  38513  nznngen  38515  trsspwALT3  39047  sspwimpALT2  39164  refsumcn  39189  iinssf  39327  icoiccdif  39750  lptioo2  39863  lptioo1  39864  icccncfext  40100  stoweidlem27  40244  stoweidlem46  40263  stoweidlem57  40274  fourierdlem40  40364  fourierdlem78  40401  ffnafv  41251  iccpartrn  41366  sprsymrelfvlem  41740  sprsymrelf1lem  41741  rnghmsscmap2  41973  rnghmsscmap  41974  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap2  42019  rhmsscmap  42020  rhmsscrnghm  42026  rngcresringcat  42030  funcringcsetc  42035  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  rhmsubcALTVlem4  42107  ssnn0ssfz  42127  lincolss  42223  lcoss  42225  lcosslsp  42227  iunord  42422