Theorem prsrcmpltd

Description: If a statement is true for all pairs of elements of a class, all pairs of elements of its complement relative to a second class, and all pairs with one element in each, then it is true for all pairs of elements of the second class. (Contributed by BTernaryTau, 27-Sep-2023)

	Ref	Expression
Hypotheses	prsrcmpltd.1	|- ( ph -> ( ( C e. A /\ D e. A ) -> ps ) )
	prsrcmpltd.2	|- ( ph -> ( ( C e. A /\ D e. ( B \ A ) ) -> ps ) )
	prsrcmpltd.3	|- ( ph -> ( ( C e. ( B \ A ) /\ D e. A ) -> ps ) )
	prsrcmpltd.4	|- ( ph -> ( ( C e. ( B \ A ) /\ D e. ( B \ A ) ) -> ps ) )
Assertion	prsrcmpltd	|- ( ph -> ( ( C e. B /\ D e. B ) -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		prsrcmpltd.1	|- ( ph -> ( ( C e. A /\ D e. A ) -> ps ) )
2		prsrcmpltd.2	|- ( ph -> ( ( C e. A /\ D e. ( B \ A ) ) -> ps ) )
3		prsrcmpltd.3	|- ( ph -> ( ( C e. ( B \ A ) /\ D e. A ) -> ps ) )
4		prsrcmpltd.4	|- ( ph -> ( ( C e. ( B \ A ) /\ D e. ( B \ A ) ) -> ps ) )
5	1	expdimp	|- ( ( ph /\ C e. A ) -> ( D e. A -> ps ) )
6	2	expdimp	|- ( ( ph /\ C e. A ) -> ( D e. ( B \ A ) -> ps ) )
7	5 6	srcmpltd	|- ( ( ph /\ C e. A ) -> ( D e. B -> ps ) )
8	7	impancom	|- ( ( ph /\ D e. B ) -> ( C e. A -> ps ) )
9	3	expdimp	|- ( ( ph /\ C e. ( B \ A ) ) -> ( D e. A -> ps ) )
10	4	expdimp	|- ( ( ph /\ C e. ( B \ A ) ) -> ( D e. ( B \ A ) -> ps ) )
11	9 10	srcmpltd	|- ( ( ph /\ C e. ( B \ A ) ) -> ( D e. B -> ps ) )
12	11	impancom	|- ( ( ph /\ D e. B ) -> ( C e. ( B \ A ) -> ps ) )
13	8 12	srcmpltd	|- ( ( ph /\ D e. B ) -> ( C e. B -> ps ) )
14	13	ex	|- ( ph -> ( D e. B -> ( C e. B -> ps ) ) )
15	14	impcomd	|- ( ph -> ( ( C e. B /\ D e. B ) -> ps ) )