Theorem ssriv 3096

Description: Inference based on subclass definition. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
ssriv.1	⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
ssriv	⊢ 𝐴 ⊆ 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssriv

Step	Hyp	Ref	Expression
1		dfss2 3081	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1429	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 1480   ⊆ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  ssid  3112  ssv  3114  difss  3197  ssun1  3234  inss1  3291  unssdif  3306  inssdif  3307  unssin  3310  inssun  3311  difindiss  3325  undif3ss  3332  0ss  3396  difprsnss  3653  snsspw  3686  pwprss  3727  pwtpss  3728  uniin  3751  iuniin  3818  iundif2ss  3873  iunpwss  3899  pwuni  4111  pwunss  4200  omsson  4521  limom  4522  xpsspw  4646  dmin  4742  dmrnssfld  4797  dmcoss  4803  dminss  4948  imainss  4949  dmxpss  4964  rnxpid  4968  mapsspm  6569  pmsspw  6570  uniixp  6608  snexxph  6831  djuss  6948  enq0enq  7232  nqnq0pi  7239  nqnq0  7242  apsscn  8402  sup3exmid  8708  zssre  9054  zsscn  9055  nnssz  9064  uzssz  9338  divfnzn  9406  zssq  9412  qssre  9415  rpssre  9445  ixxssxr  9676  ixxssixx  9678  iooval2  9691  ioossre  9711  rge0ssre  9753  fz1ssnn  9829  fzssuz  9838  fzssp1  9840  uzdisj  9866  fz0ssnn0  9889  nn0disj  9908  fzossfz  9935  fzouzsplit  9949  fzossnn  9959  fzo0ssnn0  9985  seq3coll  10578  fclim  11056  infssuzcldc  11633  prmssnn  11782  restsspw  12119  unitg  12220  cldss2  12264  blssioo  12703  tgioo  12704  limccl  12786  limcresi  12793  dvef  12845  bj-omsson  13149