Theorem disjrdx

Description: Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017)

	Ref	Expression
Hypotheses	disjrdx.1	|- ( ph -> F : A -1-1-onto-> C )
	disjrdx.2	|- ( ( ph /\ y = ( F ` x ) ) -> D = B )
Assertion	disjrdx	|- ( ph -> ( Disj_ x e. A B <-> Disj_ y e. C D ) )

Proof

Step	Hyp	Ref	Expression
1		disjrdx.1	|- ( ph -> F : A -1-1-onto-> C )
2		disjrdx.2	|- ( ( ph /\ y = ( F ` x ) ) -> D = B )
3		f1of	|- ( F : A -1-1-onto-> C -> F : A --> C )
4	1 3	syl	|- ( ph -> F : A --> C )
5	4	ffvelcdmda	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. C )
6		f1ofveu	|- ( ( F : A -1-1-onto-> C /\ y e. C ) -> E! x e. A ( F ` x ) = y )
7	1 6	sylan	|- ( ( ph /\ y e. C ) -> E! x e. A ( F ` x ) = y )
8		eqcom	|- ( ( F ` x ) = y <-> y = ( F ` x ) )
9	8	reubii	|- ( E! x e. A ( F ` x ) = y <-> E! x e. A y = ( F ` x ) )
10	7 9	sylib	|- ( ( ph /\ y e. C ) -> E! x e. A y = ( F ` x ) )
11	2	eleq2d	|- ( ( ph /\ y = ( F ` x ) ) -> ( z e. D <-> z e. B ) )
12	5 10 11	rmoxfrd	|- ( ph -> ( E* y e. C z e. D <-> E* x e. A z e. B ) )
13	12	bicomd	|- ( ph -> ( E* x e. A z e. B <-> E* y e. C z e. D ) )
14	13	albidv	|- ( ph -> ( A. z E* x e. A z e. B <-> A. z E* y e. C z e. D ) )
15		df-disj	|- ( Disj_ x e. A B <-> A. z E* x e. A z e. B )
16		df-disj	|- ( Disj_ y e. C D <-> A. z E* y e. C z e. D )
17	14 15 16	3bitr4g	|- ( ph -> ( Disj_ x e. A B <-> Disj_ y e. C D ) )