Theorem ssriv 3004

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

Syntax hints:   → wi 4   ∈ wcel 1434   ⊆ wss 2974

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987

This theorem is referenced by:  ssid  3019  ssv  3020  difss  3099  ssun1  3136  inss1  3193  unssdif  3206  inssdif  3207  unssin  3210  inssun  3211  difindiss  3225  undif3ss  3232  0ss  3289  difprsnss  3532  snsspw  3564  pwprss  3605  pwtpss  3606  uniin  3629  iuniin  3696  iundif2ss  3751  iunpwss  3772  pwuni  3971  pwunss  4046  omsson  4361  limom  4362  xpsspw  4478  dmin  4571  dmrnssfld  4623  dmcoss  4629  dminss  4768  imainss  4769  dmxpss  4783  rnxpid  4785  enq0enq  6683  nqnq0pi  6690  nqnq0  6693  zssre  8439  zsscn  8440  nnssz  8449  uzssz  8719  divfnzn  8787  zssq  8793  qssre  8796  rpssre  8825  ixxssxr  8999  ixxssixx  9001  iooval2  9014  ioossre  9034  rge0ssre  9076  fzssuz  9159  fzssp1  9161  uzdisj  9186  nn0disj  9225  fzossfz  9251  fzouzsplit  9265  fzossnn  9275  fzo0ssnn0  9301  fclim  10271  infssuzcldc  10491  prmssnn  10638  bj-omsson  10915