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	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )