Theorem ssex 5249

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 5227 (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 3909	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		ssex.1	. . . 4 ⊢ 𝐵 ∈ V
3	2	inex2 5246	. . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V
4		eleq1 2828	. . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
5	3, 4	mpbii 232	. 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V)
6	1, 5	sylbi 216	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  Vcvv 3431   ∩ cin 3891   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  ssexi  5250  ssexg  5251  intex  5265  moabex  5378  ixpiunwdom  9327  omex  9379  tcss  9502  bndrank  9600  scottex  9644  aceq3lem  9877  cfslb  10023  dcomex  10204  axdc2lem  10205  grothpw  10583  grothpwex  10584  grothomex  10586  elnp  10744  negfi  11924  hashfacenOLD  14165  limsuple  15185  limsuplt  15186  limsupbnd1  15189  o1add2  15331  o1mul2  15332  o1sub2  15333  o1dif  15337  caucvgrlem  15382  fsumo1  15522  lcmfval  16324  lcmf0val  16325  unbenlem  16607  ressbas2  16947  prdsval  17164  prdsbas  17166  rescbas  17539  rescbasOLD  17540  reschom  17541  rescco  17543  resccoOLD  17544  acsmapd  18270  issstrmgm  18335  issubmnd  18410  eqgfval  18802  dfod2  19169  ablfac1b  19671  islinds2  21018  pmatcollpw3lem  21930  2basgen  22138  prdstopn  22777  ressust  23413  rectbntr0  23993  elcncf  24050  cncfcnvcn  24086  cmssmscld  24512  cmsss  24513  ovolctb2  24654  limcfval  25034  ellimc2  25039  limcflf  25043  limcres  25048  limcun  25057  dvfval  25059  lhop2  25177  taylfval  25516  ulmval  25537  xrlimcnp  26116  axtgcont1  26827  fpwrelmap  31064  ressnm  31232  ressprs  31237  ordtrestNEW  31867  ddeval1  32198  ddeval0  32199  carsgclctunlem3  32283  bnj849  32901  msrval  33496  mclsval  33521  brsset  34187  isfne4  34525  refssfne  34543  topjoin  34550  bj-snglex  35159  mblfinlem3  35812  filbcmb  35894  cnpwstotbnd  35951  ismtyval  35954  ispsubsp  37755  ispsubclN  37947  isnumbasgrplem2  40926  rtrclex  41195  brmptiunrelexpd  41261  iunrelexp0  41280  mulcncff  43382  subcncff  43392  addcncff  43396  cncfuni  43398  divcncff  43403  etransclem1  43747  etransclem4  43750  etransclem13  43759  isvonmbl  44147  issubmgm2  45313  linccl  45724  ellcoellss  45745  elbigolo1  45872