Theorem ssriv 3184

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

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  ssid  3200  ssv  3202  difss  3286  ssun1  3323  inss1  3380  unssdif  3395  inssdif  3396  unssin  3399  inssun  3400  difindiss  3414  undif3ss  3421  0ss  3486  difprsnss  3757  snsspw  3791  pwprss  3832  pwtpss  3833  uniin  3856  iuniin  3923  iundif2ss  3979  iunpwss  4005  pwuni  4222  pwunss  4315  omsson  4646  limom  4647  xpsspw  4772  dmin  4871  dmrnssfld  4926  dmcoss  4932  dminss  5081  imainss  5082  dmxpss  5097  rnxpid  5101  mapsspm  6738  pmsspw  6739  uniixp  6777  snexxph  7011  djuss  7131  pw1on  7288  enq0enq  7493  nqnq0pi  7500  nqnq0  7503  apsscn  8668  aptap  8671  sup3exmid  8978  zssre  9327  zsscn  9328  nnssz  9337  uzssz  9615  divfnzn  9689  zssq  9695  qssre  9698  rpssre  9733  ixxssxr  9969  ixxssixx  9971  iooval2  9984  ioossre  10004  rge0ssre  10046  fz1ssnn  10125  fzssuz  10134  fzssp1  10136  uzdisj  10162  fz0ssnn0  10185  nn0disj  10207  fzossfz  10235  fzouzsplit  10249  fzossnn  10259  fzo0ssnn0  10285  seq3coll  10916  wrdexb  10929  fclim  11440  infssuzcldc  12091  prmssnn  12253  4sqlem19  12550  restsspw  12863  ringssrng  13536  subrngintm  13711  subrgintm  13742  cnsubmlem  14077  cnsubglem  14078  znf1o  14150  unitg  14241  cldss2  14285  blssioo  14732  tgioo  14733  limccl  14838  limcresi  14845  dvef  14906  plyssc  14918  reeff1o  14949  bj-omsson  15524