Theorem ssriv 3198

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

Syntax hints:   → wi 4   ∈ wcel 2177   ⊆ wss 3167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  ssid  3214  ssv  3216  difss  3300  ssun1  3337  inss1  3394  unssdif  3409  inssdif  3410  unssin  3413  inssun  3414  difindiss  3428  undif3ss  3435  0ss  3500  difprsnss  3773  snsspw  3807  pwprss  3848  pwtpss  3849  uniin  3872  iuniin  3939  iundif2ss  3995  iunpwss  4021  pwuni  4240  pwunss  4334  omsson  4665  limom  4666  xpsspw  4791  dmin  4891  dmrnssfld  4946  dmcoss  4953  dminss  5102  imainss  5103  dmxpss  5118  rnxpid  5122  mapsspm  6776  pmsspw  6777  uniixp  6815  snexxph  7059  djuss  7179  pw1on  7345  enq0enq  7551  nqnq0pi  7558  nqnq0  7561  apsscn  8727  aptap  8730  sup3exmid  9037  zssre  9386  zsscn  9387  nnssz  9396  uzssz  9675  divfnzn  9749  zssq  9755  qssre  9758  rpssre  9793  ixxssxr  10029  ixxssixx  10031  iooval2  10044  ioossre  10064  rge0ssre  10106  fz1ssnn  10185  fzssuz  10194  fzssp1  10196  uzdisj  10222  fz0ssnn0  10245  nn0disj  10267  fzossfz  10295  fzouzsplit  10310  fzossnn  10320  fzo0ssnn0  10351  infssuzcldc  10385  seq3coll  10994  wrdexb  11013  fclim  11649  bitsss  12300  prmssnn  12478  4sqlem19  12776  restsspw  13125  prdsgrpd  13485  prdsinvgd  13486  ringssrng  13843  subrngintm  14018  subrgintm  14049  cnsubmlem  14384  cnsubglem  14385  znf1o  14457  mplbasss  14502  unitg  14578  cldss2  14622  blssioo  15069  tgioo  15070  limccl  15175  limcresi  15182  dvef  15243  plyssc  15255  reeff1o  15289  bj-omsson  15972