Definition df-he

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

	Ref	Expression
Assertion	df-he	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	whe	⊢ 𝑅 hereditary 𝐴
3	0 1	cima	⊢ ( 𝑅 “ 𝐴 )
4	3 1	wss	⊢ ( 𝑅 “ 𝐴 ) ⊆ 𝐴
5	2 4	wb	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )