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  4276  pwunss  4374  omsson  4705  limom  4706  xpsspw  4831  dmin  4931  dmrnssfld  4987  dmcoss  4994  dminss  5143  imainss  5144  dmxpss  5159  rnxpid  5163  relmptopab  6213  mapsspm  6837  pmsspw  6838  uniixp  6876  snexxph  7125  djuss  7245  pw1on  7419  enq0enq  7626  nqnq0pi  7633  nqnq0  7636  apsscn  8802  aptap  8805  sup3exmid  9112  zssre  9461  zsscn  9462  nnssz  9471  uzssz  9750  divfnzn  9824  zssq  9830  qssre  9833  rpssre  9868  ixxssxr  10104  ixxssixx  10106  iooval2  10119  ioossre  10139  rge0ssre  10181  fz1ssnn  10260  fzssuz  10269  fzssp1  10271  uzdisj  10297  fz0ssnn0  10320  nn0disj  10342  fzossfz  10370  fzouzsplit  10385  fzossnn  10398  fzo0ssnn0  10429  infssuzcldc  10463  seq3coll  11072  wrdexb  11091  fclim  11813  bitsss  12464  prmssnn  12642  4sqlem19  12940  restsspw  13290  prdsgrpd  13650  prdsinvgd  13651  ringssrng  14008  subrngintm  14184  subrgintm  14215  cnsubmlem  14550  cnsubglem  14551  znf1o  14623  mplbasss  14668  unitg  14744  cldss2  14788  blssioo  15235  tgioo  15236  limccl  15341  limcresi  15348  dvef  15409  plyssc  15421  reeff1o  15455  trlsfvalg  16102  bj-omsson  16349