Theorem disjexc

Description: A variant of disjex , applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016)

	Ref	Expression
Hypothesis	disjexc.1	|- ( x = y -> A = B )
Assertion	disjexc	|- ( ( E. z ( z e. A /\ z e. B ) -> x = y ) -> ( A = B \/ ( A i^i B ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		disjexc.1	|- ( x = y -> A = B )
2	1	imim2i	|- ( ( E. z ( z e. A /\ z e. B ) -> x = y ) -> ( E. z ( z e. A /\ z e. B ) -> A = B ) )
3		orcom	|- ( ( A = B \/ -. E. z ( z e. A /\ z e. B ) ) <-> ( -. E. z ( z e. A /\ z e. B ) \/ A = B ) )
4		df-in	|- ( A i^i B ) = { z | ( z e. A /\ z e. B ) }
5	4	neeq1i	|- ( ( A i^i B ) =/= (/) <-> { z | ( z e. A /\ z e. B ) } =/= (/) )
6		abn0	|- ( { z | ( z e. A /\ z e. B ) } =/= (/) <-> E. z ( z e. A /\ z e. B ) )
7	5 6	bitr2i	|- ( E. z ( z e. A /\ z e. B ) <-> ( A i^i B ) =/= (/) )
8	7	necon2bbii	|- ( ( A i^i B ) = (/) <-> -. E. z ( z e. A /\ z e. B ) )
9	8	orbi2i	|- ( ( A = B \/ ( A i^i B ) = (/) ) <-> ( A = B \/ -. E. z ( z e. A /\ z e. B ) ) )
10		imor	|- ( ( E. z ( z e. A /\ z e. B ) -> A = B ) <-> ( -. E. z ( z e. A /\ z e. B ) \/ A = B ) )
11	3 9 10	3bitr4i	|- ( ( A = B \/ ( A i^i B ) = (/) ) <-> ( E. z ( z e. A /\ z e. B ) -> A = B ) )
12	2 11	sylibr	|- ( ( E. z ( z e. A /\ z e. B ) -> x = y ) -> ( A = B \/ ( A i^i B ) = (/) ) )