Theorem ssriv 3159

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  ssid  3175  ssv  3177  difss  3261  ssun1  3298  inss1  3355  unssdif  3370  inssdif  3371  unssin  3374  inssun  3375  difindiss  3389  undif3ss  3396  0ss  3461  difprsnss  3730  snsspw  3764  pwprss  3805  pwtpss  3806  uniin  3829  iuniin  3896  iundif2ss  3952  iunpwss  3978  pwuni  4192  pwunss  4283  omsson  4612  limom  4613  xpsspw  4738  dmin  4835  dmrnssfld  4890  dmcoss  4896  dminss  5043  imainss  5044  dmxpss  5059  rnxpid  5063  mapsspm  6681  pmsspw  6682  uniixp  6720  snexxph  6948  djuss  7068  pw1on  7224  enq0enq  7429  nqnq0pi  7436  nqnq0  7439  apsscn  8603  aptap  8606  sup3exmid  8913  zssre  9259  zsscn  9260  nnssz  9269  uzssz  9546  divfnzn  9620  zssq  9626  qssre  9629  rpssre  9663  ixxssxr  9899  ixxssixx  9901  iooval2  9914  ioossre  9934  rge0ssre  9976  fz1ssnn  10055  fzssuz  10064  fzssp1  10066  uzdisj  10092  fz0ssnn0  10115  nn0disj  10137  fzossfz  10164  fzouzsplit  10178  fzossnn  10188  fzo0ssnn0  10214  seq3coll  10821  fclim  11301  infssuzcldc  11951  prmssnn  12111  restsspw  12697  subrgintm  13362  cnsubmlem  13442  cnsubglem  13443  unitg  13532  cldss2  13576  blssioo  14015  tgioo  14016  limccl  14098  limcresi  14105  dvef  14158  reeff1o  14164  bj-omsson  14684