Theorem ssriv 3188

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

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssid  3204  ssv  3206  difss  3290  ssun1  3327  inss1  3384  unssdif  3399  inssdif  3400  unssin  3403  inssun  3404  difindiss  3418  undif3ss  3425  0ss  3490  difprsnss  3761  snsspw  3795  pwprss  3836  pwtpss  3837  uniin  3860  iuniin  3927  iundif2ss  3983  iunpwss  4009  pwuni  4226  pwunss  4319  omsson  4650  limom  4651  xpsspw  4776  dmin  4875  dmrnssfld  4930  dmcoss  4936  dminss  5085  imainss  5086  dmxpss  5101  rnxpid  5105  mapsspm  6750  pmsspw  6751  uniixp  6789  snexxph  7025  djuss  7145  pw1on  7311  enq0enq  7517  nqnq0pi  7524  nqnq0  7527  apsscn  8693  aptap  8696  sup3exmid  9003  zssre  9352  zsscn  9353  nnssz  9362  uzssz  9640  divfnzn  9714  zssq  9720  qssre  9723  rpssre  9758  ixxssxr  9994  ixxssixx  9996  iooval2  10009  ioossre  10029  rge0ssre  10071  fz1ssnn  10150  fzssuz  10159  fzssp1  10161  uzdisj  10187  fz0ssnn0  10210  nn0disj  10232  fzossfz  10260  fzouzsplit  10274  fzossnn  10284  fzo0ssnn0  10310  infssuzcldc  10344  seq3coll  10953  wrdexb  10966  fclim  11478  bitsss  12129  prmssnn  12307  4sqlem19  12605  restsspw  12953  prdsgrpd  13313  prdsinvgd  13314  ringssrng  13671  subrngintm  13846  subrgintm  13877  cnsubmlem  14212  cnsubglem  14213  znf1o  14285  mplbasss  14330  unitg  14406  cldss2  14450  blssioo  14897  tgioo  14898  limccl  15003  limcresi  15010  dvef  15071  plyssc  15083  reeff1o  15117  bj-omsson  15716