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	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → 𝜓 ) )
	prsrcmpltd.2	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝜓 ) )
	prsrcmpltd.3	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝜓 ) )
	prsrcmpltd.4	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝜓 ) )
Assertion	prsrcmpltd	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		prsrcmpltd.1	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) → 𝜓 ) )
2		prsrcmpltd.2	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝜓 ) )
3		prsrcmpltd.3	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝐷 ∈ 𝐴 ) → 𝜓 ) )
4		prsrcmpltd.4	⊢ ( 𝜑 → ( ( 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝜓 ) )
5	1	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ 𝐴 → 𝜓 ) )
6	2	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) → 𝜓 ) )
7	5 6	srcmpltd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ 𝐵 → 𝜓 ) )
8	7	impancom	⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∈ 𝐴 → 𝜓 ) )
9	3	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐷 ∈ 𝐴 → 𝜓 ) )
10	4	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐷 ∈ ( 𝐵 ∖ 𝐴 ) → 𝜓 ) )
11	9 10	srcmpltd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐷 ∈ 𝐵 → 𝜓 ) )
12	11	impancom	⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∈ ( 𝐵 ∖ 𝐴 ) → 𝜓 ) )
13	8 12	srcmpltd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∈ 𝐵 → 𝜓 ) )
14	13	ex	⊢ ( 𝜑 → ( 𝐷 ∈ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝜓 ) ) )
15	14	impcomd	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → 𝜓 ) )