Theorem ssriv 3241

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

Syntax hints:   → wi 4   ∈ wcel 2203   ⊆ wss 3210

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  ssid  3257  ssv  3259  difss  3344  ssun1  3381  inss1  3440  unssdif  3455  inssdif  3456  unssin  3459  inssun  3460  difindiss  3474  undif3ss  3481  0ss  3546  difprsnss  3831  snsspw  3867  pwprss  3909  pwtpss  3910  uniin  3933  iuniin  4000  iundif2ss  4056  iunpwss  4082  pwuni  4304  pwunss  4403  omsson  4734  limom  4735  xpsspw  4861  dmin  4963  dmrnssfld  5019  dmcoss  5026  dminss  5176  imainss  5177  dmxpss  5192  rnxpid  5196  relmptopab  6255  mapsspm  6915  pmsspw  6916  uniixp  6955  snexxph  7219  djuss  7360  pw1on  7535  enq0enq  7742  nqnq0pi  7749  nqnq0  7752  apsscn  8917  aptap  8920  sup3exmid  9227  zssre  9580  zsscn  9581  nnssz  9590  uzssz  9870  divfnzn  9949  zssq  9955  qssre  9958  rpssre  9993  ixxssxr  10229  ixxssixx  10231  iooval2  10244  ioossre  10264  rge0ssre  10306  fz1ssnn  10386  fzssuz  10395  fzssp1  10397  uzdisj  10423  fz0ssnn0  10446  nn0disj  10468  fzossfz  10496  fzouzsplit  10511  fzossnn  10525  fzo0ssnn0  10556  infssuzcldc  10591  hashfibc  11200  seq3coll  11207  wrdexb  11229  fclim  11972  bitsss  12624  prmssnn  12802  4sqlem19  13100  restsspw  13451  prdsgrpd  13811  prdsinvgd  13812  ringssrng  14170  subrngintm  14346  subrgintm  14377  cnsubmlem  14713  cnsubglem  14714  znf1o  14786  mplbasss  14838  unitg  14914  cldss2  14958  blssioo  15405  tgioo  15406  limccl  15511  limcresi  15518  dvef  15579  plyssc  15591  reeff1o  15625  griedg0ssusgr  16233  trlsfvalg  16365  clwwlksswrd  16379  clwwlksclwwlkn  16392  bj-omsson  16719