Theorem disjeq2

Description: Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	disjeq2	|- ( A. x e. A B = C -> ( Disj_ x e. A B <-> Disj_ x e. A C ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss2	|- ( B = C -> C C_ B )
2	1	ralimi	|- ( A. x e. A B = C -> A. x e. A C C_ B )
3		disjss2	|- ( A. x e. A C C_ B -> ( Disj_ x e. A B -> Disj_ x e. A C ) )
4	2 3	syl	|- ( A. x e. A B = C -> ( Disj_ x e. A B -> Disj_ x e. A C ) )
5		eqimss	|- ( B = C -> B C_ C )
6	5	ralimi	|- ( A. x e. A B = C -> A. x e. A B C_ C )
7		disjss2	|- ( A. x e. A B C_ C -> ( Disj_ x e. A C -> Disj_ x e. A B ) )
8	6 7	syl	|- ( A. x e. A B = C -> ( Disj_ x e. A C -> Disj_ x e. A B ) )
9	4 8	impbid	|- ( A. x e. A B = C -> ( Disj_ x e. A B <-> Disj_ x e. A C ) )