Theorem ssriv 3160

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

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  ssid  3176  ssv  3178  difss  3262  ssun1  3299  inss1  3356  unssdif  3371  inssdif  3372  unssin  3375  inssun  3376  difindiss  3390  undif3ss  3397  0ss  3462  difprsnss  3731  snsspw  3765  pwprss  3806  pwtpss  3807  uniin  3830  iuniin  3897  iundif2ss  3953  iunpwss  3979  pwuni  4193  pwunss  4284  omsson  4613  limom  4614  xpsspw  4739  dmin  4836  dmrnssfld  4891  dmcoss  4897  dminss  5044  imainss  5045  dmxpss  5060  rnxpid  5064  mapsspm  6682  pmsspw  6683  uniixp  6721  snexxph  6949  djuss  7069  pw1on  7225  enq0enq  7430  nqnq0pi  7437  nqnq0  7440  apsscn  8604  aptap  8607  sup3exmid  8914  zssre  9260  zsscn  9261  nnssz  9270  uzssz  9547  divfnzn  9621  zssq  9627  qssre  9630  rpssre  9664  ixxssxr  9900  ixxssixx  9902  iooval2  9915  ioossre  9935  rge0ssre  9977  fz1ssnn  10056  fzssuz  10065  fzssp1  10067  uzdisj  10093  fz0ssnn0  10116  nn0disj  10138  fzossfz  10165  fzouzsplit  10179  fzossnn  10189  fzo0ssnn0  10215  seq3coll  10822  fclim  11302  infssuzcldc  11952  prmssnn  12112  restsspw  12698  subrgintm  13364  cnsubmlem  13475  cnsubglem  13476  unitg  13565  cldss2  13609  blssioo  14048  tgioo  14049  limccl  14131  limcresi  14138  dvef  14191  reeff1o  14197  bj-omsson  14717