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  4329  pwunss  4428  omsson  4760  limom  4761  xpsspw  4887  dmin  4989  dmrnssfld  5045  dmcoss  5052  dminss  5202  imainss  5203  dmxpss  5218  rnxpid  5222  relmptopab  6291  mapfoss  6947  fsetsspwxp  6948  mapsspm  6963  pmsspw  6964  uniixp  7003  snexxph  7267  djuss  7410  pw1on  7585  enq0enq  7798  nqnq0pi  7805  nqnq0  7808  apsscn  8976  aptap  8979  sup3exmid  9288  zssre  9653  zsscn  9654  nnssz  9663  uzssz  9944  divfnzn  10023  zssq  10029  qssre  10032  rpssre  10067  ixxssxr  10304  ixxssixx  10306  iooval2  10319  ioossre  10339  rge0ssre  10381  fzssz  10432  fz1ssnn  10464  fzssuz  10473  fzssp1  10475  uzdisj  10502  fz0ssnn0  10525  nn0disj  10547  fzossfz  10575  fzouzsplit  10590  fzossnn  10604  fzo0ssnn0  10635  infssuzcldc  10670  hashfibc  11285  seq3coll  11296  wrdexb  11318  fclim  12062  bitsss  12714  prmssnn  12892  4sqlem19  13190  restsspw  13605  prdsgrpd  14199  prdsinvgd  14200  ringssrng  14344  subrngintm  14522  subrgintm  14553  cnsubmlem  14917  cnsubglem  14918  znf1o  14988  mplbasss  15089  unitg  15165  cldss2  15209  blssioo  15656  tgioo  15657  limccl  15762  limcresi  15769  dvef  15830  plyssc  15842  reeff1o  15876  griedg0ssusgr  16504  trlsfvalg  16636  clwwlksswrd  16650  clwwlksclwwlkn  16663  bj-omsson  17000