Theorem ssrdv 2122

Description: Deduction rule based on subclass definition.

Hypothesis

Ref	Expression
ssrdv.1	⊢ (φ → (x ∈ A → x ∈ B))

Assertion

Ref	Expression
ssrdv	⊢ (φ → A ⊆ B)

Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (φ → (x ∈ A → x ∈ B))
2	1	19.21aiv 1324	. 2 ⊢ (φ → ∀x(x ∈ A → x ∈ B))
3		dfss2 2110	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
4	2, 3	sylibr 198	1 ⊢ (φ → A ⊆ B)

Syntax hints:   → wi 3  ∀wal 990   ∈ wcel 994   ⊆ wss 2099

This theorem is referenced by:  sscon 2223  ssdif 2224  difsn 2528  prss 2536  tpss 2541  intss1 2615  intmin 2620  intssuni 2622  ss2iun 2645  ssiun2 2661  sspwb 2835  pwssun 2905  tron 2998  tz7.7 3001  ssorduni 3147  onint 3152  limsssuc 3204  limuni3 3206  limomss 3224  relop 3365  dmss 3401  ssrnres 3566  chfnrn 3916  dff3 3931  fo1stres 4156  fo2ndres 4157  onfununi 4209  tz7.48-1 4257  tz7.49 4260  oaass 4331  ss2ixp 4495  mapenlem2 4637  pssnn 4681  inf3lemd 4757  inf3lem1 4758  inf3lem6 4763  r1tr 4800  zorn2lem4 4937  zorn2lem5 4938  unxpdomlem 4993  carduni 5008  genpss 5261  distrlem1pr 5281  distrlem5pr 5285  ltexprlem2 5297  ltexprlem6 5301  ltexprlem7 5302  reclem3pr 5312  reclem4pr 5313  suppsrlem 5375  suprelem 5413  iccssre 6523  uzss 6558  infxpidmlem7 7770  infxpidmlem8 7771  bastg 7834  tgtop 7840  tgss 7848  tgss2 7849  basgen2 7851  clslp 7958  cnsscnp 7982  cncnplem2 7985  ssbl 8065  blssopn 8077  unirnbl 8085  metcnss 8109  cmsss 8208  grplactf1o 8339  ubthlem2 8788  psdmrn 8910  ococss 9442  shsub1 9564  shlessi 9623  shmodsi 9638  spansnss 9770  spanpr 9779  spansnm0i 9873  pjjsi 9923  sumdmdii 10624  sumdmdlem 10627  sumdmdlem2 10628  cdj3lem1 10643  uninqs 10730  clsrebb 10993  nsn 11017  rdmob 11202  rcmob 11203  xpss1 11403  xpss2 11404  ordtypelem4 11430  ordtypelem7 11433  hartog 11436  onsdom 11437  omsubindss 11449  subntr 11482  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  cncomp 11494  alexsublem3 11498  subtopmetlem 11505  reconnlem1 11507  iccconn 11514  topfneec 11562  fnessref 11564  locfincomp 11575  comppfsc 11578  neibastop2lem1 11580  neibastop2lem2 11581  fnejoin1 11591  fnejoin2 11592  ist1-3 11604  fgss 11634  fbssfg 11635  fgbas 11636  fgid 11637  fgmin 11639  fbfgss 11640  isufil2 11650  filufint 11659  uffixfr 11660  ufcondr 11666  flimopn 11679  cnpfillim 11686  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  sfcls 11716  filclus 11717  flimfcls 11725  uffclsflim 11728  tailmap 11759  tailuni 11761  tailfb 11762  filnet 11768  ssga 11777  gapm 11784  inficl 11849  fzfi 11864  lpss2 11906  metsstop 11909  blhalf 11911  iccss 11920  tx1cn 11976  tx2cn 11977  sstotbnd 11992  totbndss 11993  ismtybndlem 12008  heiborlem11 12021  recms 12066  rrntotbnd 12078  iccbnd 12082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain