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 - start with the Axiom of Extensionality The difference, union, and intersection of two classes Combinations of difference, union, and intersection of two classes dfss5
Description: Alternate definition of subclass relationship: a class A is a
subclass of another class B iff each element of A is equal to an
element of B . (Contributed by AV , 13-Nov-2020)
Ref
Expression
Assertion
dfss5 ⊢ A ⊆ B ↔ ∀ x ∈ A ∃ y ∈ B x = y
Proof
Step
Hyp
Ref
Expression
1
dfss3 ⊢ A ⊆ B ↔ ∀ x ∈ A x ∈ B
2
clel5 ⊢ x ∈ B ↔ ∃ y ∈ B x = y
3
2
ralbii ⊢ ∀ x ∈ A x ∈ B ↔ ∀ x ∈ A ∃ y ∈ B x = y
4
1 3
bitri ⊢ A ⊆ B ↔ ∀ x ∈ A ∃ y ∈ B x = y