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

Metamath Proof Explorer

Theorem ssdmral

Description: Subclass of a domain. (Contributed by Peter Mazsa, 15-Sep-2018)

Ref Expression
Assertion ssdmral ⊢ A ⊆ dom ⁡ R ↔ ∀ x ∈ A ∃ y x R y

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ A ⊆ dom ⁡ R ↔ ∀ x ∈ A x ∈ dom ⁡ R
2 eldmg ⊢ x ∈ V → x ∈ dom ⁡ R ↔ ∃ y x R y
3 2 elv ⊢ x ∈ dom ⁡ R ↔ ∃ y x R y
4 3 ralbii ⊢ ∀ x ∈ A x ∈ dom ⁡ R ↔ ∀ x ∈ A ∃ y x R y
5 1 4 bitri ⊢ A ⊆ dom ⁡ R ↔ ∀ x ∈ A ∃ y x R y