This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfss3f

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004)

Ref Expression
Hypotheses dfssf.1 ⊢ Ⅎ _ x A
dfssf.2 ⊢ Ⅎ _ x B
Assertion dfss3f ⊢ A ⊆ B ↔ ∀ x ∈ A x ∈ B

Proof

Step Hyp Ref Expression
1 dfssf.1 ⊢ Ⅎ _ x A
2 dfssf.2 ⊢ Ⅎ _ x B
3 1 2 dfssf ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B
4 df-ral ⊢ ∀ x ∈ A x ∈ B ↔ ∀ x x ∈ A → x ∈ B
5 3 4 bitr4i ⊢ A ⊆ B ↔ ∀ x ∈ A x ∈ B