Theorem ssriv 3132

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 3117	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1433	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 2128   ⊆ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  ssid  3148  ssv  3150  difss  3233  ssun1  3270  inss1  3327  unssdif  3342  inssdif  3343  unssin  3346  inssun  3347  difindiss  3361  undif3ss  3368  0ss  3432  difprsnss  3694  snsspw  3727  pwprss  3768  pwtpss  3769  uniin  3792  iuniin  3859  iundif2ss  3914  iunpwss  3940  pwuni  4153  pwunss  4243  omsson  4571  limom  4572  xpsspw  4697  dmin  4793  dmrnssfld  4848  dmcoss  4854  dminss  4999  imainss  5000  dmxpss  5015  rnxpid  5019  mapsspm  6624  pmsspw  6625  uniixp  6663  snexxph  6891  djuss  7008  pw1on  7155  enq0enq  7345  nqnq0pi  7352  nqnq0  7355  apsscn  8516  sup3exmid  8822  zssre  9168  zsscn  9169  nnssz  9178  uzssz  9452  divfnzn  9523  zssq  9529  qssre  9532  rpssre  9564  ixxssxr  9797  ixxssixx  9799  iooval2  9812  ioossre  9832  rge0ssre  9874  fz1ssnn  9951  fzssuz  9960  fzssp1  9962  uzdisj  9988  fz0ssnn0  10011  nn0disj  10030  fzossfz  10057  fzouzsplit  10071  fzossnn  10081  fzo0ssnn0  10107  seq3coll  10706  fclim  11184  infssuzcldc  11830  prmssnn  11980  restsspw  12332  unitg  12433  cldss2  12477  blssioo  12916  tgioo  12917  limccl  12999  limcresi  13006  dvef  13059  reeff1o  13065  bj-omsson  13508