Theorem ssex 2715

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 2699 (a.k.a. Subset Axiom).

Hypothesis

Ref	Expression
ssex.1	⊢ B ∈ V

Assertion

Ref	Expression
ssex	⊢ (A ⊆ B → A ∈ V)

Proof of Theorem ssex

Step	Hyp	Ref	Expression
1		df-ss 2049	. 2 ⊢ (A ⊆ B ↔ (A ∩ B) = A)
2		ssex.1	. . . 4 ⊢ B ∈ V
3	2	inex2 2713	. . 3 ⊢ (A ∩ B) ∈ V
4		eleq1 1531	. . 3 ⊢ ((A ∩ B) = A → ((A ∩ B) ∈ V ↔ A ∈ V))
5	3, 4	mpbii 193	. 2 ⊢ ((A ∩ B) = A → A ∈ V)
6	1, 5	sylbi 199	1 ⊢ (A ⊆ B → A ∈ V)

Syntax hints:   → wi 3   = wceq 954   ∈ wcel 956  Vcvv 1807   ∩ cin 2042   ⊆ wss 2043

This theorem is referenced by:  ssexi 2716  ssexg 2717  intex 2725  elpm 4337  mapss 4347  inf3lem7 4611  omex 4619  unbnnt 4631  bndrank 4674  scottex 4708  zorn2lem4 4783  ondomon 4848  elnp 5084  suplem2pr 5154  lbinfm 6015  elcncf 7220  unbenlem 7467  lpval 7705  lmclim 7926  sh 9052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2699

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain