Theorem ssriv 3208

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

Syntax hints:   → wi 4   ∈ wcel 2180   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  ssid  3224  ssv  3226  difss  3310  ssun1  3347  inss1  3404  unssdif  3419  inssdif  3420  unssin  3423  inssun  3424  difindiss  3438  undif3ss  3445  0ss  3510  difprsnss  3785  snsspw  3821  pwprss  3863  pwtpss  3864  uniin  3887  iuniin  3954  iundif2ss  4010  iunpwss  4036  pwuni  4255  pwunss  4351  omsson  4682  limom  4683  xpsspw  4808  dmin  4908  dmrnssfld  4963  dmcoss  4970  dminss  5119  imainss  5120  dmxpss  5135  rnxpid  5139  mapsspm  6799  pmsspw  6800  uniixp  6838  snexxph  7085  djuss  7205  pw1on  7379  enq0enq  7586  nqnq0pi  7593  nqnq0  7596  apsscn  8762  aptap  8765  sup3exmid  9072  zssre  9421  zsscn  9422  nnssz  9431  uzssz  9710  divfnzn  9784  zssq  9790  qssre  9793  rpssre  9828  ixxssxr  10064  ixxssixx  10066  iooval2  10079  ioossre  10099  rge0ssre  10141  fz1ssnn  10220  fzssuz  10229  fzssp1  10231  uzdisj  10257  fz0ssnn0  10280  nn0disj  10302  fzossfz  10330  fzouzsplit  10345  fzossnn  10357  fzo0ssnn0  10388  infssuzcldc  10422  seq3coll  11031  wrdexb  11050  fclim  11771  bitsss  12422  prmssnn  12600  4sqlem19  12898  restsspw  13248  prdsgrpd  13608  prdsinvgd  13609  ringssrng  13966  subrngintm  14141  subrgintm  14172  cnsubmlem  14507  cnsubglem  14508  znf1o  14580  mplbasss  14625  unitg  14701  cldss2  14745  blssioo  15192  tgioo  15193  limccl  15298  limcresi  15305  dvef  15366  plyssc  15378  reeff1o  15412  bj-omsson  16235