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

Proof

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