Theorem relfldext

Description: The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	relfldext	|- Rel /FldExt

Proof

Step	Hyp	Ref	Expression
1		df-fldext	|- /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }
2	1	relopabiv	|- Rel /FldExt