Theorem ssex 1700

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way of expressing the Axiom of Separation zfaus 1480 (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 1492	. 2 ⊢ (A ⊆ B ↔ (A ∩ B) = A)
2		ssex.1	. . . 4 ⊢ B ∈ V
3	2	inex2 1698	. . 3 ⊢ (A ∩ B) ∈ V
4		eleq1 1149	. . 3 ⊢ ((A ∩ B) = A → ((A ∩ B) ∈ V ↔ A ∈ V))
5	3, 4	mpbii 168	. 2 ⊢ ((A ∩ B) = A → A ∈ V)
6	1, 5	sylbi 174	1 ⊢ (A ⊆ B → A ∈ V)

Syntax hints:   → wi 2   = wceq 1091   ∈ wcel 1092  Vcvv 1348   ∩ cin 1486   ⊆ wss 1487

This theorem is referenced by:  ssexi 1701  ssexg 1702  intex 1986  mapss 3270  inf3lem7 3470  omex 3475  bndrank 3526  scottex 3541  zornlem4 3606  ondomon 3662  elnp 3886  suplem2pr 3956  sh 5116

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492

metamath.org