Metamath Proof Explorer


Theorem sshepw

Description: The relation between sets and their subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020)

Ref Expression
Assertion sshepw [⊂] -1 I hereditary 𝒫 A

Proof

Step Hyp Ref Expression
1 psshepw [⊂] -1 hereditary 𝒫 A
2 idhe I hereditary 𝒫 A
3 unhe1 [⊂] -1 hereditary 𝒫 A I hereditary 𝒫 A [⊂] -1 I hereditary 𝒫 A
4 1 2 3 mp2an [⊂] -1 I hereditary 𝒫 A