Theorem disjeq1f

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

	Ref	Expression
Hypotheses	disjss1f.1	|- F/_ x A
	disjss1f.2	|- F/_ x B
Assertion	disjeq1f	|- ( A = B -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )

Proof

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