This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Replacement Theorems requiring subset and intersection existence ssex
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 (a.k.a.
Subset Axiom). (Contributed by NM , 27-Apr-1994)
Ref
Expression
Hypothesis
ssex.1 ⊢ 𝐵 ∈ V
Assertion
ssex ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
Proof
Step
Hyp
Ref
Expression
1
ssex.1 ⊢ 𝐵 ∈ V
2
dfss2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
3
1
inex2 ⊢ ( 𝐴 ∩ 𝐵 ) ∈ V
4
eleq1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∈ V ↔ 𝐴 ∈ V ) )
5
3 4
mpbii ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → 𝐴 ∈ V )
6
2 5
sylbi ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )