Theorem disjeq0

Description: Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022)

	Ref	Expression
Assertion	disjeq0	|- ( ( A i^i B ) = (/) -> ( A = B <-> ( A = (/) /\ B = (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ineq1	|- ( A = B -> ( A i^i B ) = ( B i^i B ) )
2		inidm	|- ( B i^i B ) = B
3	1 2	eqtrdi	|- ( A = B -> ( A i^i B ) = B )
4	3	eqeq1d	|- ( A = B -> ( ( A i^i B ) = (/) <-> B = (/) ) )
5		eqtr	|- ( ( A = B /\ B = (/) ) -> A = (/) )
6		simpr	|- ( ( A = B /\ B = (/) ) -> B = (/) )
7	5 6	jca	|- ( ( A = B /\ B = (/) ) -> ( A = (/) /\ B = (/) ) )
8	7	ex	|- ( A = B -> ( B = (/) -> ( A = (/) /\ B = (/) ) ) )
9	4 8	sylbid	|- ( A = B -> ( ( A i^i B ) = (/) -> ( A = (/) /\ B = (/) ) ) )
10	9	com12	|- ( ( A i^i B ) = (/) -> ( A = B -> ( A = (/) /\ B = (/) ) ) )
11		eqtr3	|- ( ( A = (/) /\ B = (/) ) -> A = B )
12	10 11	impbid1	|- ( ( A i^i B ) = (/) -> ( A = B <-> ( A = (/) /\ B = (/) ) ) )