Metamath Proof Explorer


Theorem disjxun0

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

Ref Expression
Hypothesis disjxun0.1 ( ( 𝜑𝑥𝐵 ) → 𝐶 = ∅ )
Assertion disjxun0 ( 𝜑 → ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶Disj 𝑥𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 disjxun0.1 ( ( 𝜑𝑥𝐵 ) → 𝐶 = ∅ )
2 nel02 ( 𝐶 = ∅ → ¬ 𝑦𝐶 )
3 1 2 syl ( ( 𝜑𝑥𝐵 ) → ¬ 𝑦𝐶 )
4 3 rmounid ( 𝜑 → ( ∃* 𝑥 ∈ ( 𝐴𝐵 ) 𝑦𝐶 ↔ ∃* 𝑥𝐴 𝑦𝐶 ) )
5 4 albidv ( 𝜑 → ( ∀ 𝑦 ∃* 𝑥 ∈ ( 𝐴𝐵 ) 𝑦𝐶 ↔ ∀ 𝑦 ∃* 𝑥𝐴 𝑦𝐶 ) )
6 df-disj ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶 ↔ ∀ 𝑦 ∃* 𝑥 ∈ ( 𝐴𝐵 ) 𝑦𝐶 )
7 df-disj ( Disj 𝑥𝐴 𝐶 ↔ ∀ 𝑦 ∃* 𝑥𝐴 𝑦𝐶 )
8 5 6 7 3bitr4g ( 𝜑 → ( Disj 𝑥 ∈ ( 𝐴𝐵 ) 𝐶Disj 𝑥𝐴 𝐶 ) )