Theorem ssex 5279

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 5248 (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		dfss2 3924	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5276	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2852	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 235	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144  Vcvv 3456   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923

This theorem is referenced by:  ssexi  5280  ssexg  5281  intex  5302  moabexOLD  5428  naddunif  8666  ixpiunwdom  9540  omex  9600  tcss  9699  bndrank  9801  scottex  9845  aceq3lem  10078  cfslb  10225  dcomex  10406  axdc2lem  10407  grothpw  10786  grothpwex  10787  grothomex  10789  elnp  10947  negfi  12143  limsuple  15507  limsuplt  15508  limsupbnd1  15511  o1add2  15653  o1mul2  15654  o1sub2  15655  o1dif  15659  caucvgrlem  15702  fsumo1  15842  lcmfval  16657  lcmf0val  16658  unbenlem  16946  ressbas2  17276  prdsval  17486  prdsbas  17488  rescbas  17864  reschom  17865  rescco  17867  acsmapd  18588  issstrmgm  18689  issubmgm2  18739  issubmnd  18797  eqgfval  19219  dfod2  19606  ablfac1b  20114  islinds2  21867  pmatcollpw3lem  22845  2basgen  23052  prdstopn  23690  ressust  24325  rectbntr0  24895  elcncf  24953  cncfcnvcn  24989  cmssmscld  25414  cmsss  25415  ovolctb2  25556  limcfval  25936  ellimc2  25941  limcflf  25945  limcres  25950  limcun  25959  dvfval  25961  lhop2  26079  taylfval  26424  ulmval  26445  xrlimcnp  27035  axtgcont1  28639  ressnm  33144  ressprs  33146  ordtrestNEW  34220  ddeval1  34533  ddeval0  34534  carsgclctunlem3  34619  bnj849  35222  msrval  35893  mclsval  35918  brsset  36242  isfne4  36705  refssfne  36723  topjoin  36730  bj-snglex  37463  mblfinlem3  38163  filbcmb  38244  cnpwstotbnd  38301  ismtyval  38304  ispsubsp  40374  ispsubclN  40566  isnumbasgrplem2  43686  rtrclex  44198  brmptiunrelexpd  44264  iunrelexp0  44283  mulcncff  46449  subcncff  46459  addcncff  46463  cncfuni  46465  divcncff  46470  etransclem1  46814  etransclem4  46817  etransclem13  46826  isvonmbl  47217  isubgriedg  48490  isubgrvtx  48494  uhgrimisgrgric  48558  linccl  49041  ellcoellss  49062  elbigolo1  49184