Theorem ssriv 3228

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssid  3244  ssv  3246  difss  3330  ssun1  3367  inss1  3424  unssdif  3439  inssdif  3440  unssin  3443  inssun  3444  difindiss  3458  undif3ss  3465  0ss  3530  difprsnss  3806  snsspw  3842  pwprss  3884  pwtpss  3885  uniin  3908  iuniin  3975  iundif2ss  4031  iunpwss  4057  pwuni  4277  pwunss  4375  omsson  4706  limom  4707  xpsspw  4833  dmin  4934  dmrnssfld  4990  dmcoss  4997  dminss  5146  imainss  5147  dmxpss  5162  rnxpid  5166  relmptopab  6216  mapsspm  6842  pmsspw  6843  uniixp  6881  snexxph  7133  djuss  7253  pw1on  7427  enq0enq  7634  nqnq0pi  7641  nqnq0  7644  apsscn  8810  aptap  8813  sup3exmid  9120  zssre  9469  zsscn  9470  nnssz  9479  uzssz  9759  divfnzn  9833  zssq  9839  qssre  9842  rpssre  9877  ixxssxr  10113  ixxssixx  10115  iooval2  10128  ioossre  10148  rge0ssre  10190  fz1ssnn  10269  fzssuz  10278  fzssp1  10280  uzdisj  10306  fz0ssnn0  10329  nn0disj  10351  fzossfz  10379  fzouzsplit  10394  fzossnn  10407  fzo0ssnn0  10438  infssuzcldc  10472  seq3coll  11082  wrdexb  11101  fclim  11826  bitsss  12477  prmssnn  12655  4sqlem19  12953  restsspw  13303  prdsgrpd  13663  prdsinvgd  13664  ringssrng  14021  subrngintm  14197  subrgintm  14228  cnsubmlem  14563  cnsubglem  14564  znf1o  14636  mplbasss  14681  unitg  14757  cldss2  14801  blssioo  15248  tgioo  15249  limccl  15354  limcresi  15361  dvef  15422  plyssc  15434  reeff1o  15468  griedg0ssusgr  16070  trlsfvalg  16153  clwwlksswrd  16166  clwwlksclwwlkn  16179  bj-omsson  16434