Theorem ssex 4730

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4709 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
ssex.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ssex	⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		df-ss 3554	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 4728	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2676	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 222	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 206	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  ssexi  4731  ssexg  4732  intex  4747  moabex  4854  ixpiunwdom  8379  omex  8423  tcss  8503  bndrank  8587  scottex  8631  aceq3lem  8826  cfslb  8971  dcomex  9152  axdc2lem  9153  grothpw  9527  grothpwex  9528  grothomex  9530  elnp  9688  negfi  10850  hashfacen  13095  limsuple  14057  limsuplt  14058  limsupbnd1  14061  o1add2  14202  o1mul2  14203  o1sub2  14204  o1dif  14208  caucvgrlem  14251  fsumo1  14385  lcmfval  15172  lcmf0val  15173  unbenlem  15450  ressbas2  15758  prdsval  15938  prdsbas  15940  rescbas  16312  reschom  16313  rescco  16315  acsmapd  17001  issstrmgm  17075  issubmnd  17141  eqgfval  17465  dfod2  17804  ablfac1b  18292  islinds2  19971  pmatcollpw3lem  20407  2basgen  20605  prdstopn  21241  ressust  21878  rectbntr0  22443  elcncf  22500  cncfcnvcn  22532  cmsss  22955  ovolctb2  23067  limcfval  23442  ellimc2  23447  limcflf  23451  limcres  23456  limcun  23465  dvfval  23467  lhop2  23582  taylfval  23917  ulmval  23938  xrlimcnp  24495  axtgcont1  25167  fpwrelmap  28896  ressnm  28982  ressprs  28986  ordtrestNEW  29295  ddeval1  29624  ddeval0  29625  carsgclctunlem3  29709  bnj849  30249  msrval  30689  mclsval  30714  brsset  31166  isfne4  31505  refssfne  31523  topjoin  31530  bj-snglex  32154  mblfinlem3  32618  filbcmb  32705  cnpwstotbnd  32766  ismtyval  32769  ispsubsp  34049  ispsubclN  34241  isnumbasgrplem2  36693  rtrclex  36943  brmptiunrelexpd  36994  iunrelexp0  37013  mulcncff  38753  subcncff  38765  addcncff  38770  cncfuni  38772  divcncff  38777  etransclem1  39128  etransclem4  39131  etransclem13  39140  isvonmbl  39528  issubmgm2  41580  linccl  41997  ellcoellss  42018  elbigolo1  42149