Theorem elnelun

Description: The union of 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 yields the original set. (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	elnelun	⊢ ( 𝐸 ∪ 𝑁 ) = 𝐴

Proof

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