This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )