Theorem undisjrab

Description: Union of two disjoint restricted class abstractions; compare unrab . (Contributed by Steve Rodriguez, 28-Feb-2020)

	Ref	Expression
Assertion	undisjrab	⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ∅ ↔ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		rabeq0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝜑 ∧ 𝜓 ) )
2		df-nan	⊢ ( ( 𝜑 ⊼ 𝜓 ) ↔ ¬ ( 𝜑 ∧ 𝜓 ) )
3		nanorxor	⊢ ( ( 𝜑 ⊼ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
4	2 3	bitr3i	⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
5	4	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) )
6		rabbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) ) ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } )
7	1 5 6	3bitri	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) } = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } )
8		inrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) }
9	8	eqeq1i	⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ 𝜓 ) } = ∅ )
10		unrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) }
11	10	eqeq1i	⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } )
12	7 9 11	3bitr4i	⊢ ( ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ∅ ↔ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ⊻ 𝜓 ) } )