Theorem ssdmral

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

	Ref	Expression
Assertion	ssdmral	⊢ ( 𝐴 ⊆ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝑅 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dfss3	⊢ ( 𝐴 ⊆ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝑅 )
2		eldmg	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 ) )
3	2	elv	⊢ ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑥 𝑅 𝑦 )
4	3	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝑅 𝑦 )
5	1 4	bitri	⊢ ( 𝐴 ⊆ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝑅 𝑦 )