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 
|- ( `' [C.] u. _I ) hereditary ~P A

Proof

Step Hyp Ref Expression
1 psshepw 
 |-  `' [C.] hereditary ~P A
2 idhe 
 |-  _I hereditary ~P A
3 unhe1 
 |-  ( ( `' [C.] hereditary ~P A /\ _I hereditary ~P A ) -> ( `' [C.] u. _I ) hereditary ~P A )
4 1 2 3 mp2an 
 |-  ( `' [C.] u. _I ) hereditary ~P A