Theorem ssriv 3230

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

Syntax hints:   → wi 4   ∈ wcel 2201   ⊆ wss 3199

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  ssid  3246  ssv  3248  difss  3332  ssun1  3369  inss1  3426  unssdif  3441  inssdif  3442  unssin  3445  inssun  3446  difindiss  3460  undif3ss  3467  0ss  3532  difprsnss  3812  snsspw  3848  pwprss  3890  pwtpss  3891  uniin  3914  iuniin  3981  iundif2ss  4037  iunpwss  4063  pwuni  4284  pwunss  4382  omsson  4713  limom  4714  xpsspw  4840  dmin  4941  dmrnssfld  4997  dmcoss  5004  dminss  5153  imainss  5154  dmxpss  5169  rnxpid  5173  relmptopab  6229  mapsspm  6856  pmsspw  6857  uniixp  6895  snexxph  7154  djuss  7274  pw1on  7449  enq0enq  7656  nqnq0pi  7663  nqnq0  7666  apsscn  8832  aptap  8835  sup3exmid  9142  zssre  9491  zsscn  9492  nnssz  9501  uzssz  9781  divfnzn  9860  zssq  9866  qssre  9869  rpssre  9904  ixxssxr  10140  ixxssixx  10142  iooval2  10155  ioossre  10175  rge0ssre  10217  fz1ssnn  10296  fzssuz  10305  fzssp1  10307  uzdisj  10333  fz0ssnn0  10356  nn0disj  10378  fzossfz  10406  fzouzsplit  10421  fzossnn  10435  fzo0ssnn0  10466  infssuzcldc  10501  seq3coll  11112  wrdexb  11134  fclim  11877  bitsss  12529  prmssnn  12707  4sqlem19  13005  restsspw  13355  prdsgrpd  13715  prdsinvgd  13716  ringssrng  14074  subrngintm  14250  subrgintm  14281  cnsubmlem  14616  cnsubglem  14617  znf1o  14689  mplbasss  14739  unitg  14815  cldss2  14859  blssioo  15306  tgioo  15307  limccl  15412  limcresi  15419  dvef  15480  plyssc  15492  reeff1o  15526  griedg0ssusgr  16131  trlsfvalg  16263  clwwlksswrd  16277  clwwlksclwwlkn  16290  bj-omsson  16617