Theorem disjxun0

Description: Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypothesis	disjxun0.1	$$⊢\left(\phi \wedge x\in B\right)\to C=\varnothing$$
Assertion	disjxun0	$$⊢\phi \to \left(\underset{x\in A\cup B}{Disj}C\leftrightarrow \underset{x\in A}{Disj}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjxun0.1	$$⊢\left(\phi \wedge x\in B\right)\to C=\varnothing$$
2		nel02	$$⊢C=\varnothing \to \neg y\in C$$
3	1 2	syl	$$⊢\left(\phi \wedge x\in B\right)\to \neg y\in C$$
4	3	rmounid	$$⊢\phi \to \left({\exists }^{*}x\in \left(A\cup B\right)y\in C\leftrightarrow {\exists }^{*}x\in Ay\in C\right)$$
5	4	albidv	$$⊢\phi \to \left(\forall y{\exists }^{*}x\in \left(A\cup B\right)y\in C\leftrightarrow \forall y{\exists }^{*}x\in Ay\in C\right)$$
6		df-disj	$$⊢\underset{x\in A\cup B}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in \left(A\cup B\right)y\in C$$
7		df-disj	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in Ay\in C$$
8	5 6 7	3bitr4g	$$⊢\phi \to \left(\underset{x\in A\cup B}{Disj}C\leftrightarrow \underset{x\in A}{Disj}C\right)$$