Theorem ssriv 3252

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

Syntax hints:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssid  3268  ssv  3270  difss  3355  ssun1  3392  inss1  3451  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  difindiss  3485  undif3ss  3492  0ss  3561  difprsnss  3851  snsspw  3887  pwprss  3929  pwtpss  3930  uniin  3953  iuniin  4020  iundif2ss  4076  iunpwss  4102  pwuni  4327  pwunss  4426  omsson  4758  limom  4759  xpsspw  4885  dmin  4987  dmrnssfld  5043  dmcoss  5050  dminss  5200  imainss  5201  dmxpss  5216  rnxpid  5220  relmptopab  6285  mapfoss  6941  fsetsspwxp  6942  mapsspm  6957  pmsspw  6958  uniixp  6997  snexxph  7261  djuss  7404  pw1on  7579  enq0enq  7792  nqnq0pi  7799  nqnq0  7802  apsscn  8969  aptap  8972  sup3exmid  9281  zssre  9634  zsscn  9635  nnssz  9644  uzssz  9925  divfnzn  10004  zssq  10010  qssre  10013  rpssre  10048  ixxssxr  10285  ixxssixx  10287  iooval2  10300  ioossre  10320  rge0ssre  10362  fzssz  10413  fz1ssnn  10445  fzssuz  10454  fzssp1  10456  uzdisj  10483  fz0ssnn0  10506  nn0disj  10528  fzossfz  10556  fzouzsplit  10571  fzossnn  10585  fzo0ssnn0  10616  infssuzcldc  10651  hashfibc  11266  seq3coll  11277  wrdexb  11299  fclim  12043  bitsss  12695  prmssnn  12873  4sqlem19  13171  restsspw  13586  prdsgrpd  14180  prdsinvgd  14181  ringssrng  14325  subrngintm  14503  subrgintm  14534  cnsubmlem  14898  cnsubglem  14899  znf1o  14969  mplbasss  15070  unitg  15146  cldss2  15190  blssioo  15637  tgioo  15638  limccl  15743  limcresi  15750  dvef  15811  plyssc  15823  reeff1o  15857  griedg0ssusgr  16475  trlsfvalg  16607  clwwlksswrd  16621  clwwlksclwwlkn  16634  bj-omsson  16971