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 𝑥 ∈ { ( 𝐴 ∖ 𝐵 ) , ( 𝐴 ∩ 𝐵 ) } 𝑥 )