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

Metamath Proof Explorer

Theorem disjdifprg2

Description: A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion disjdifprg2 ( 𝐴 ∈ 𝑉 → Disj 𝑥 ∈ { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 )

Proof

Step Hyp Ref Expression
1 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )
2 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3 disjdifprg ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ V ∧ 𝐴 ∈ V ) → Disj 𝑥 ∈ { ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 )
4 1 2 3 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → Disj 𝑥 ∈ { ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 )
5 difin ⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
6 5 preq1i ⊢ { ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) , ( 𝐴 ∩ 𝐵 ) } = { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) }
7 6 a1i ⊢ ( 𝐴 ∈ 𝑉 → { ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) , ( 𝐴 ∩ 𝐵 ) } = { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) } )
8 7 disjeq1d ⊢ ( 𝐴 ∈ 𝑉 → ( Disj 𝑥 ∈ { ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 ↔ Disj 𝑥 ∈ { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 ) )
9 4 8 mpbid ⊢ ( 𝐴 ∈ 𝑉 → Disj 𝑥 ∈ { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 )