Theorem clublem

Description: If a superset Y of X possesses the property parameterized in x in ps , then Y is a superset of the closure of that property for the set X . (Contributed by RP, 23-Jul-2020)

	Ref	Expression
Hypotheses	clublem.y	|- ( ph -> Y e. _V )
	clublem.sub	|- ( x = Y -> ( ps <-> ch ) )
	clublem.sup	|- ( ph -> X C_ Y )
	clublem.maj	|- ( ph -> ch )
Assertion	clublem	|- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ Y )

Proof

Step	Hyp	Ref	Expression
1		clublem.y	|- ( ph -> Y e. _V )
2		clublem.sub	|- ( x = Y -> ( ps <-> ch ) )
3		clublem.sup	|- ( ph -> X C_ Y )
4		clublem.maj	|- ( ph -> ch )
5	1	a1d	|- ( ph -> ( ( X C_ Y /\ ch ) -> Y e. _V ) )
6	2	cleq2lem	|- ( x = Y -> ( ( X C_ x /\ ps ) <-> ( X C_ Y /\ ch ) ) )
7	6	elab3g	|- ( ( ( X C_ Y /\ ch ) -> Y e. _V ) -> ( Y e. { x | ( X C_ x /\ ps ) } <-> ( X C_ Y /\ ch ) ) )
8	5 7	syl	|- ( ph -> ( Y e. { x | ( X C_ x /\ ps ) } <-> ( X C_ Y /\ ch ) ) )
9	3 4 8	mpbir2and	|- ( ph -> Y e. { x | ( X C_ x /\ ps ) } )
10		intss1	|- ( Y e. { x | ( X C_ x /\ ps ) } -> |^| { x | ( X C_ x /\ ps ) } C_ Y )
11	9 10	syl	|- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ Y )