Theorem subrfld

Description: A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	subrfld.1	|- ( ph -> R e. Field )
	subrfld.2	|- ( ph -> S e. ( SubRing ` R ) )
Assertion	subrfld	|- ( ph -> ( R |`s S ) e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		subrfld.1	|- ( ph -> R e. Field )
2		subrfld.2	|- ( ph -> S e. ( SubRing ` R ) )
3		fldidom	|- ( R e. Field -> R e. IDomn )
4	1 3	syl	|- ( ph -> R e. IDomn )
5	4 2	subridom	|- ( ph -> ( R |`s S ) e. IDomn )