Theorem ssriv 2072

Description: Inference rule based on subclass definition.

Hypothesis

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

Assertion

Ref	Expression
ssriv	⊢ A ⊆ B

Distinct variable groups:   x,A   x,B

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 2061	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
2		ssriv.1	. 2 ⊢ (x ∈ A → x ∈ B)
3	1, 2	mpgbir 990	1 ⊢ A ⊆ B

Syntax hints:   → wi 3   ∈ wcel 960   ⊆ wss 2050

This theorem is referenced by:  ssv 2084  difss 2170  ssun1 2196  inss1 2233  0ss 2305  difprsn 2469  snsspw 2483  uniin 2524  iuniin 2577  iunpwss 2623  unipw 2762  pwuni 2763  pwunss 2832  omsson 3142  omssnlim 3151  xpss 3236  dmin 3324  dmrnssfld 3363  dminss 3468  imainss 3469  mapsspm 4345  uniixp 4363  ixpssmap 4369  pwfilem 4577  pwfilemOLD 4578  dfom3 4639  tz9.12lem1 4669  rankun 4701  alephsson 4905  cardcf 4923  cfeq0 4926  1pr 5129  reclem2pr 5169  zssre 6144  zsscn 6145  nnssz 6153  zssq 6262  qssre 6265  rpssre 6286  ioossre 6390  ioossicc 6398  fzssuzt 6506  reeff1olem1 7424  reeff1o 7426  ntrss2 7687  qdensere 7748  blssioo 7910  tgioo 7912  sspval 8378  phrel 8470  bnrel 8523  ubthlem6 8530  hlrel 8590  pilem2 8667  efifolem4 8720  eff1i 8739  effoi 8740  resslogrn 8748  chsscm 9107  chcmh 9108  hhssnv 9129  omlsi 9240  choc1 9286  shunss 9332  shslej 9333  shsub1 9336  shsub2 9337  shsidm 9352  spanun 9462  spansn 9475  5oalem7 9600  3oalem3 9604  mayete3 9668  hmopex 9797  cnlnssadj 10008  adjbdlnt 10011  adjsslnop 10015  shatomistic 10283  hatomistic 10284

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain