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

Proof

Step	Hyp	Ref	Expression
1		dfss2f.1	⊢ Ⅎ 𝑥 𝐴
2		dfss2f.2	⊢ Ⅎ 𝑥 𝐵
3	1 2	dfss2f	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
4		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
5	3 4	bitr4i	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )