Theorem ssriv 3229

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

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

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 3204  df-ss 3211

This theorem is referenced by:  ssid  3245  ssv  3247  difss  3331  ssun1  3368  inss1  3425  unssdif  3440  inssdif  3441  unssin  3444  inssun  3445  difindiss  3459  undif3ss  3466  0ss  3531  difprsnss  3809  snsspw  3845  pwprss  3887  pwtpss  3888  uniin  3911  iuniin  3978  iundif2ss  4034  iunpwss  4060  pwuni  4280  pwunss  4378  omsson  4709  limom  4710  xpsspw  4836  dmin  4937  dmrnssfld  4993  dmcoss  5000  dminss  5149  imainss  5150  dmxpss  5165  rnxpid  5169  relmptopab  6219  mapsspm  6846  pmsspw  6847  uniixp  6885  snexxph  7143  djuss  7263  pw1on  7437  enq0enq  7644  nqnq0pi  7651  nqnq0  7654  apsscn  8820  aptap  8823  sup3exmid  9130  zssre  9479  zsscn  9480  nnssz  9489  uzssz  9769  divfnzn  9848  zssq  9854  qssre  9857  rpssre  9892  ixxssxr  10128  ixxssixx  10130  iooval2  10143  ioossre  10163  rge0ssre  10205  fz1ssnn  10284  fzssuz  10293  fzssp1  10295  uzdisj  10321  fz0ssnn0  10344  nn0disj  10366  fzossfz  10394  fzouzsplit  10409  fzossnn  10422  fzo0ssnn0  10453  infssuzcldc  10488  seq3coll  11099  wrdexb  11118  fclim  11848  bitsss  12499  prmssnn  12677  4sqlem19  12975  restsspw  13325  prdsgrpd  13685  prdsinvgd  13686  ringssrng  14043  subrngintm  14219  subrgintm  14250  cnsubmlem  14585  cnsubglem  14586  znf1o  14658  mplbasss  14703  unitg  14779  cldss2  14823  blssioo  15270  tgioo  15271  limccl  15376  limcresi  15383  dvef  15444  plyssc  15456  reeff1o  15490  griedg0ssusgr  16095  trlsfvalg  16192  clwwlksswrd  16206  clwwlksclwwlkn  16219  bj-omsson  16507