Theorem ssriv 3183

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

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

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 3159  df-ss 3166

This theorem is referenced by:  ssid  3199  ssv  3201  difss  3285  ssun1  3322  inss1  3379  unssdif  3394  inssdif  3395  unssin  3398  inssun  3399  difindiss  3413  undif3ss  3420  0ss  3485  difprsnss  3756  snsspw  3790  pwprss  3831  pwtpss  3832  uniin  3855  iuniin  3922  iundif2ss  3978  iunpwss  4004  pwuni  4221  pwunss  4314  omsson  4645  limom  4646  xpsspw  4771  dmin  4870  dmrnssfld  4925  dmcoss  4931  dminss  5080  imainss  5081  dmxpss  5096  rnxpid  5100  mapsspm  6736  pmsspw  6737  uniixp  6775  snexxph  7009  djuss  7129  pw1on  7286  enq0enq  7491  nqnq0pi  7498  nqnq0  7501  apsscn  8666  aptap  8669  sup3exmid  8976  zssre  9324  zsscn  9325  nnssz  9334  uzssz  9612  divfnzn  9686  zssq  9692  qssre  9695  rpssre  9730  ixxssxr  9966  ixxssixx  9968  iooval2  9981  ioossre  10001  rge0ssre  10043  fz1ssnn  10122  fzssuz  10131  fzssp1  10133  uzdisj  10159  fz0ssnn0  10182  nn0disj  10204  fzossfz  10232  fzouzsplit  10246  fzossnn  10256  fzo0ssnn0  10282  seq3coll  10913  wrdexb  10926  fclim  11437  infssuzcldc  12088  prmssnn  12250  4sqlem19  12547  restsspw  12860  ringssrng  13533  subrngintm  13708  subrgintm  13739  cnsubmlem  14066  cnsubglem  14067  znf1o  14139  unitg  14230  cldss2  14274  blssioo  14713  tgioo  14714  limccl  14813  limcresi  14820  dvef  14873  plyssc  14885  reeff1o  14908  bj-omsson  15454