Theorem ssriv 2974

Description: Inference rule 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 2959	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		ssriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1356	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ∈ wcel 1407   ⊆ wss 2942

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-11 1411  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-in 2949  df-ss 2956

This theorem is referenced by:  ssid  2989  ssv  2990  difss  3095  ssun1  3131  inss1  3182  unssdif  3197  inssdif  3198  unssin  3201  inssun  3202  difindiss  3216  undif3ss  3223  0ss  3280  difprsnss  3527  snsspw  3560  pwprss  3601  pwtpss  3602  uniin  3625  iuniin  3692  iundif2ss  3747  iunpwss  3768  pwuni  3968  pwunss  4045  omsson  4360  limom  4361  xpsspw  4475  dmin  4568  dmrnssfld  4620  dmcoss  4626  dminss  4763  imainss  4764  dmxpss  4778  rnxpid  4780  enq0enq  6557  nqnq0pi  6564  nqnq0  6567  zssre  8279  zsscn  8280  nnssz  8289  uzssz  8558  divfnzn  8623  zssq  8629  qssre  8632  rpssre  8661  ixxssxr  8840  ixxssixx  8842  iooval2  8855  ioossre  8875  rge0ssre  8917  fzssuz  9000  fzssp1  9002  uzdisj  9027  nn0disj  9067  fzossfz  9093  fzouzsplit  9107  fzossnn  9117  fzo0ssnn0  9143  fclim  10009  bj-omsson  10417