elneldisj

Description: The set of elements s determining classes C (which may depend on s ) containing a special element and the set of elements s determining classes C not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 9-Nov-2020) (Revised by AV, 17-Dec-2021)

	Ref	Expression
Hypotheses	elneldisj.e	⊢ 𝐸 = { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }
	elneldisj.n	⊢ 𝑁 = { 𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶 }
Assertion	elneldisj	⊢ ( 𝐸 ∩ 𝑁 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		elneldisj.e	⊢ 𝐸 = { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }
2		elneldisj.n	⊢ 𝑁 = { 𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶 }
3		df-nel	⊢ ( 𝐵 ∉ 𝐶 ↔ ¬ 𝐵 ∈ 𝐶 )
4	3	rabbii	⊢ { 𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶 } = { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 }
5	2 4	eqtri	⊢ 𝑁 = { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 }
6	1 5	ineq12i	⊢ ( 𝐸 ∩ 𝑁 ) = ( { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 } ∩ { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 } )
7		rabnc	⊢ ( { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 } ∩ { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 } ) = ∅
8	6 7	eqtri	⊢ ( 𝐸 ∩ 𝑁 ) = ∅

Metamath Proof Explorer

Theorem elneldisj

Proof