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	2 3	rabbieq	⊢ 𝑁 = { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 }
5	1 4	uneq12i	⊢ ( 𝐸 ∪ 𝑁 ) = ( { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 } ∪ { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 } )
6		rabxm	⊢ 𝐴 = ( { 𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 } ∪ { 𝑠 ∈ 𝐴 ∣ ¬ 𝐵 ∈ 𝐶 } )
7	5 6	eqtr4i	⊢ ( 𝐸 ∪ 𝑁 ) = 𝐴