Theorem ssriv 3171

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

Syntax hints:   → wi 4   ∈ wcel 2158   ⊆ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  ssid  3187  ssv  3189  difss  3273  ssun1  3310  inss1  3367  unssdif  3382  inssdif  3383  unssin  3386  inssun  3387  difindiss  3401  undif3ss  3408  0ss  3473  difprsnss  3742  snsspw  3776  pwprss  3817  pwtpss  3818  uniin  3841  iuniin  3908  iundif2ss  3964  iunpwss  3990  pwuni  4204  pwunss  4295  omsson  4624  limom  4625  xpsspw  4750  dmin  4847  dmrnssfld  4902  dmcoss  4908  dminss  5055  imainss  5056  dmxpss  5071  rnxpid  5075  mapsspm  6695  pmsspw  6696  uniixp  6734  snexxph  6962  djuss  7082  pw1on  7238  enq0enq  7443  nqnq0pi  7450  nqnq0  7453  apsscn  8617  aptap  8620  sup3exmid  8927  zssre  9273  zsscn  9274  nnssz  9283  uzssz  9560  divfnzn  9634  zssq  9640  qssre  9643  rpssre  9677  ixxssxr  9913  ixxssixx  9915  iooval2  9928  ioossre  9948  rge0ssre  9990  fz1ssnn  10069  fzssuz  10078  fzssp1  10080  uzdisj  10106  fz0ssnn0  10129  nn0disj  10151  fzossfz  10178  fzouzsplit  10192  fzossnn  10202  fzo0ssnn0  10228  seq3coll  10835  fclim  11315  infssuzcldc  11965  prmssnn  12125  restsspw  12715  ringssrng  13284  subrngintm  13427  subrgintm  13458  cnsubmlem  13729  cnsubglem  13730  unitg  13833  cldss2  13877  blssioo  14316  tgioo  14317  limccl  14399  limcresi  14406  dvef  14459  reeff1o  14465  bj-omsson  14985