Theorem intabssd

Description: When for each element y there is a subset A which may substituted for x such that y satisfying ch implies x satisfies ps then the intersection of all x that satisfy ps is a subclass the intersection of all y that satisfy ch . (Contributed by RP, 17-Oct-2020)

	Ref	Expression
Hypotheses	intabssd.ex	|- ( ph -> A e. V )
	intabssd.sub	|- ( ( ph /\ x = A ) -> ( ch -> ps ) )
	intabssd.ss	|- ( ph -> A C_ y )
Assertion	intabssd	|- ( ph -> |^| { x | ps } C_ |^| { y | ch } )

Proof

Step	Hyp	Ref	Expression
1		intabssd.ex	|- ( ph -> A e. V )
2		intabssd.sub	|- ( ( ph /\ x = A ) -> ( ch -> ps ) )
3		intabssd.ss	|- ( ph -> A C_ y )
4		eleq2	|- ( x = A -> ( z e. x <-> z e. A ) )
5	4	biimpd	|- ( x = A -> ( z e. x -> z e. A ) )
6	3	sseld	|- ( ph -> ( z e. A -> z e. y ) )
7	5 6	sylan9r	|- ( ( ph /\ x = A ) -> ( z e. x -> z e. y ) )
8	2 7	imim12d	|- ( ( ph /\ x = A ) -> ( ( ps -> z e. x ) -> ( ch -> z e. y ) ) )
9	1 8	spcimdv	|- ( ph -> ( A. x ( ps -> z e. x ) -> ( ch -> z e. y ) ) )
10	9	alrimdv	|- ( ph -> ( A. x ( ps -> z e. x ) -> A. y ( ch -> z e. y ) ) )
11		vex	|- z e. _V
12	11	elintab	|- ( z e. |^| { x | ps } <-> A. x ( ps -> z e. x ) )
13	11	elintab	|- ( z e. |^| { y | ch } <-> A. y ( ch -> z e. y ) )
14	10 12 13	3imtr4g	|- ( ph -> ( z e. |^| { x | ps } -> z e. |^| { y | ch } ) )
15	14	ssrdv	|- ( ph -> |^| { x | ps } C_ |^| { y | ch } )