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 ⊢ Ⅎ 𝑥 𝐴
dfssf.2 ⊢ Ⅎ 𝑥 𝐵
Assertion dfssf ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dfssf.1 ⊢ Ⅎ 𝑥 𝐴
2 dfssf.2 ⊢ Ⅎ 𝑥 𝐵
3 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
4 1 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
5 2 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐵
6 4 5 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 )
7 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 )
8 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
9 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
10 8 9 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
11 6 7 10 cbvalv1 ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
12 3 11 bitri ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )