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

Metamath Proof Explorer

Theorem dfssf

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994) (Revised by Andrew Salmon, 27-Aug-2011) Avoid ax-13 . (Revised by GG, 19-May-2023)

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

Proof

Step Hyp Ref Expression
1 dfssf.1 ⊢ Ⅎ _ x A
2 dfssf.2 ⊢ Ⅎ _ x B
3 df-ss ⊢ A ⊆ B ↔ ∀ z z ∈ A → z ∈ B
4 1 nfcri ⊢ Ⅎ x z ∈ A
5 2 nfcri ⊢ Ⅎ x z ∈ B
6 4 5 nfim ⊢ Ⅎ x z ∈ A → z ∈ B
7 nfv ⊢ Ⅎ z x ∈ A → x ∈ B
8 eleq1w ⊢ z = x → z ∈ A ↔ x ∈ A
9 eleq1w ⊢ z = x → z ∈ B ↔ x ∈ B
10 8 9 imbi12d ⊢ z = x → z ∈ A → z ∈ B ↔ x ∈ A → x ∈ B
11 6 7 10 cbvalv1 ⊢ ∀ z z ∈ A → z ∈ B ↔ ∀ x x ∈ A → x ∈ B
12 3 11 bitri ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B