Theorem disjeq12d

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

	Ref	Expression
Hypotheses	disjeq1d.1	|- ( ph -> A = B )
	disjeq12d.1	|- ( ph -> C = D )
Assertion	disjeq12d	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B D ) )

Proof

Step	Hyp	Ref	Expression
1		disjeq1d.1	|- ( ph -> A = B )
2		disjeq12d.1	|- ( ph -> C = D )
3	1	disjeq1d	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )
4	2	adantr	|- ( ( ph /\ x e. B ) -> C = D )
5	4	disjeq2dv	|- ( ph -> ( Disj_ x e. B C <-> Disj_ x e. B D ) )
6	3 5	bitrd	|- ( ph -> ( Disj_ x e. A C <-> Disj_ x e. B D ) )