Theorem srcmpltd

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

	Ref	Expression
Hypotheses	srcmpltd.1	|- ( ph -> ( C e. A -> ps ) )
	srcmpltd.2	|- ( ph -> ( C e. ( B \ A ) -> ps ) )
Assertion	srcmpltd	|- ( ph -> ( C e. B -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		srcmpltd.1	|- ( ph -> ( C e. A -> ps ) )
2		srcmpltd.2	|- ( ph -> ( C e. ( B \ A ) -> ps ) )
3		elun2	|- ( C e. B -> C e. ( A u. B ) )
4		undif2	|- ( A u. ( B \ A ) ) = ( A u. B )
5	3 4	eleqtrrdi	|- ( C e. B -> C e. ( A u. ( B \ A ) ) )
6		elunant	|- ( ( C e. ( A u. ( B \ A ) ) -> ps ) <-> ( ( C e. A -> ps ) /\ ( C e. ( B \ A ) -> ps ) ) )
7	1 2 6	sylanbrc	|- ( ph -> ( C e. ( A u. ( B \ A ) ) -> ps ) )
8	5 7	syl5	|- ( ph -> ( C e. B -> ps ) )