Theorem disjxun0

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

	Ref	Expression
Hypothesis	disjxun0.1	|- ( ( ph /\ x e. B ) -> C = (/) )
Assertion	disjxun0	|- ( ph -> ( Disj_ x e. ( A u. B ) C <-> Disj_ x e. A C ) )

Proof

Step	Hyp	Ref	Expression
1		disjxun0.1	|- ( ( ph /\ x e. B ) -> C = (/) )
2		nel02	|- ( C = (/) -> -. y e. C )
3	1 2	syl	|- ( ( ph /\ x e. B ) -> -. y e. C )
4	3	rmounid	|- ( ph -> ( E* x e. ( A u. B ) y e. C <-> E* x e. A y e. C ) )
5	4	albidv	|- ( ph -> ( A. y E* x e. ( A u. B ) y e. C <-> A. y E* x e. A y e. C ) )
6		df-disj	|- ( Disj_ x e. ( A u. B ) C <-> A. y E* x e. ( A u. B ) y e. C )
7		df-disj	|- ( Disj_ x e. A C <-> A. y E* x e. A y e. C )
8	5 6 7	3bitr4g	|- ( ph -> ( Disj_ x e. ( A u. B ) C <-> Disj_ x e. A C ) )