Theorem ssriv 3252

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  ssid  3268  ssv  3270  difss  3355  ssun1  3392  inss1  3451  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  difindiss  3485  undif3ss  3492  0ss  3561  difprsnss  3853  snsspw  3889  pwprss  3931  pwtpss  3932  uniin  3955  iuniin  4022  iundif2ss  4078  iunpwss  4104  pwuni  4331  pwunss  4430  omsson  4762  limom  4763  xpsspw  4889  dmin  4991  dmrnssfld  5047  dmcoss  5054  dminss  5205  imainss  5206  dmxpss  5221  rnxpid  5225  relmptopab  6294  mapfoss  6951  fsetsspwxp  6952  mapsspm  6967  pmsspw  6968  uniixp  7008  snexxph  7273  djuss  7417  pw1on  7592  enq0enq  7805  nqnq0pi  7812  nqnq0  7815  apsscn  8984  aptap  8987  sup3exmid  9296  zssre  9663  zsscn  9664  nnssz  9673  uzssz  9959  divfnzn  10038  zssq  10044  qssre  10047  rpssre  10083  ixxssxr  10320  ixxssixx  10322  iooval2  10335  ioossre  10355  rge0ssre  10397  fzssz  10448  fz1ssnn  10480  fzssuz  10489  fzssp1  10491  uzdisj  10518  fz0ssnn0  10541  nn0disj  10563  fzossfz  10591  fzouzsplit  10606  fzossnn  10620  fzo0ssnn0  10651  infssuzcldc  10686  hashfibc  11306  seq3coll  11317  wrdexb  11339  fclim  12086  bitsss  12738  prmssnn  12916  4sqlem19  13218  restsspw  13663  cntzssv  14161  prdsgrpd  14305  prdsinvgd  14306  ringssrng  14450  subrngintm  14630  subrgintm  14661  cnsubmlem  15025  cnsubglem  15026  znf1o  15096  mplbasss  15224  unitg  15300  cldss2  15344  blssioo  15791  tgioo  15792  limccl  15897  limcresi  15904  dvef  15965  plyssc  15977  reeff1o  16011  griedg0ssusgr  16709  trlsfvalg  16841  clwwlksswrd  16855  clwwlksclwwlkn  16868  bj-omsson  17205