Theorem undisjrab

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

	Ref	Expression
Assertion	undisjrab	|- ( ( { x e. A | ph } i^i { x e. A | ps } ) = (/) <-> ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/_ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		rabeq0	|- ( { x e. A | ( ph /\ ps ) } = (/) <-> A. x e. A -. ( ph /\ ps ) )
2		df-nan	|- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
3		nanorxor	|- ( ( ph -/\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
4	2 3	bitr3i	|- ( -. ( ph /\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
5	4	ralbii	|- ( A. x e. A -. ( ph /\ ps ) <-> A. x e. A ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
6		rabbi	|- ( A. x e. A ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) <-> { x e. A | ( ph \/ ps ) } = { x e. A | ( ph \/_ ps ) } )
7	1 5 6	3bitri	|- ( { x e. A | ( ph /\ ps ) } = (/) <-> { x e. A | ( ph \/ ps ) } = { x e. A | ( ph \/_ ps ) } )
8		inrab	|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }
9	8	eqeq1i	|- ( ( { x e. A | ph } i^i { x e. A | ps } ) = (/) <-> { x e. A | ( ph /\ ps ) } = (/) )
10		unrab	|- ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/ ps ) }
11	10	eqeq1i	|- ( ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/_ ps ) } <-> { x e. A | ( ph \/ ps ) } = { x e. A | ( ph \/_ ps ) } )
12	7 9 11	3bitr4i	|- ( ( { x e. A | ph } i^i { x e. A | ps } ) = (/) <-> ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/_ ps ) } )