Theorem ssriv 3244

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

Syntax hints:   → wi 4   ∈ wcel 2205   ⊆ wss 3213

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  ssid  3260  ssv  3262  difss  3347  ssun1  3384  inss1  3443  unssdif  3458  inssdif  3459  unssin  3462  inssun  3463  difindiss  3477  undif3ss  3484  0ss  3549  difprsnss  3834  snsspw  3870  pwprss  3912  pwtpss  3913  uniin  3936  iuniin  4003  iundif2ss  4059  iunpwss  4085  pwuni  4307  pwunss  4406  omsson  4737  limom  4738  xpsspw  4864  dmin  4966  dmrnssfld  5022  dmcoss  5029  dminss  5179  imainss  5180  dmxpss  5195  rnxpid  5199  relmptopab  6258  mapsspm  6918  pmsspw  6919  uniixp  6958  snexxph  7222  djuss  7363  pw1on  7538  enq0enq  7751  nqnq0pi  7758  nqnq0  7761  apsscn  8926  aptap  8929  sup3exmid  9236  zssre  9589  zsscn  9590  nnssz  9599  uzssz  9880  divfnzn  9959  zssq  9965  qssre  9968  rpssre  10003  ixxssxr  10239  ixxssixx  10241  iooval2  10254  ioossre  10274  rge0ssre  10316  fz1ssnn  10396  fzssuz  10405  fzssp1  10407  uzdisj  10434  fz0ssnn0  10457  nn0disj  10479  fzossfz  10507  fzouzsplit  10522  fzossnn  10536  fzo0ssnn0  10567  infssuzcldc  10602  hashfibc  11215  seq3coll  11222  wrdexb  11244  fclim  11987  bitsss  12639  prmssnn  12817  4sqlem19  13115  restsspw  13483  prdsgrpd  13843  prdsinvgd  13844  ringssrng  14202  subrngintm  14380  subrgintm  14411  cnsubmlem  14775  cnsubglem  14776  znf1o  14848  mplbasss  14900  unitg  14976  cldss2  15020  blssioo  15467  tgioo  15468  limccl  15573  limcresi  15580  dvef  15641  plyssc  15653  reeff1o  15687  griedg0ssusgr  16295  trlsfvalg  16427  clwwlksswrd  16441  clwwlksclwwlkn  16454  bj-omsson  16781