Theorem dfhe2

Description: The property of relation R being hereditary in class A . (Contributed by RP, 27-Mar-2020)

	Ref	Expression
Assertion	dfhe2	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-he	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
2		resssxp	⊢ ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ↔ ( 𝑅 ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )
3	1 2	bitri	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) )