Theorem reuxfrdf

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfrd (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017) (Revised by Thierry Arnoux, 30-Mar-2018)

	Ref	Expression
Hypotheses	reuxfrdf.0	|- F/_ y B
	reuxfrdf.1	|- ( ( ph /\ y e. C ) -> A e. B )
	reuxfrdf.2	|- ( ( ph /\ x e. B ) -> E* y e. C x = A )
Assertion	reuxfrdf	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C ps ) )

Proof

Step	Hyp	Ref	Expression
1		reuxfrdf.0	|- F/_ y B
2		reuxfrdf.1	|- ( ( ph /\ y e. C ) -> A e. B )
3		reuxfrdf.2	|- ( ( ph /\ x e. B ) -> E* y e. C x = A )
4		rmoan	|- ( E* y e. C x = A -> E* y e. C ( ps /\ x = A ) )
5	3 4	syl	|- ( ( ph /\ x e. B ) -> E* y e. C ( ps /\ x = A ) )
6		ancom	|- ( ( ps /\ x = A ) <-> ( x = A /\ ps ) )
7	6	rmobii	|- ( E* y e. C ( ps /\ x = A ) <-> E* y e. C ( x = A /\ ps ) )
8	5 7	sylib	|- ( ( ph /\ x e. B ) -> E* y e. C ( x = A /\ ps ) )
9	8	ralrimiva	|- ( ph -> A. x e. B E* y e. C ( x = A /\ ps ) )
10		df-rmo	|- ( E* y e. C ( x = A /\ ps ) <-> E* y ( y e. C /\ ( x = A /\ ps ) ) )
11	10	ralbii	|- ( A. x e. B E* y e. C ( x = A /\ ps ) <-> A. x e. B E* y ( y e. C /\ ( x = A /\ ps ) ) )
12		df-ral	|- ( A. x e. B E* y ( y e. C /\ ( x = A /\ ps ) ) <-> A. x ( x e. B -> E* y ( y e. C /\ ( x = A /\ ps ) ) ) )
13	1	nfcri	|- F/ y x e. B
14	13	moanim	|- ( E* y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) <-> ( x e. B -> E* y ( y e. C /\ ( x = A /\ ps ) ) ) )
15	14	albii	|- ( A. x E* y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) <-> A. x ( x e. B -> E* y ( y e. C /\ ( x = A /\ ps ) ) ) )
16	12 15	bitr4i	|- ( A. x e. B E* y ( y e. C /\ ( x = A /\ ps ) ) <-> A. x E* y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
17		2euswapv	|- ( A. x E* y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) -> ( E! x E. y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) -> E! y E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) ) )
18		df-reu	|- ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! x ( x e. B /\ E. y e. C ( x = A /\ ps ) ) )
19	13	r19.41	|- ( E. y e. C ( ( x = A /\ ps ) /\ x e. B ) <-> ( E. y e. C ( x = A /\ ps ) /\ x e. B ) )
20		ancom	|- ( ( x e. B /\ ( x = A /\ ps ) ) <-> ( ( x = A /\ ps ) /\ x e. B ) )
21	20	rexbii	|- ( E. y e. C ( x e. B /\ ( x = A /\ ps ) ) <-> E. y e. C ( ( x = A /\ ps ) /\ x e. B ) )
22		ancom	|- ( ( x e. B /\ E. y e. C ( x = A /\ ps ) ) <-> ( E. y e. C ( x = A /\ ps ) /\ x e. B ) )
23	19 21 22	3bitr4i	|- ( E. y e. C ( x e. B /\ ( x = A /\ ps ) ) <-> ( x e. B /\ E. y e. C ( x = A /\ ps ) ) )
24		df-rex	|- ( E. y e. C ( x e. B /\ ( x = A /\ ps ) ) <-> E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
25	23 24	bitr3i	|- ( ( x e. B /\ E. y e. C ( x = A /\ ps ) ) <-> E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
26		an12	|- ( ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) <-> ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
27	26	exbii	|- ( E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) <-> E. y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
28	25 27	bitri	|- ( ( x e. B /\ E. y e. C ( x = A /\ ps ) ) <-> E. y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
29	28	eubii	|- ( E! x ( x e. B /\ E. y e. C ( x = A /\ ps ) ) <-> E! x E. y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
30	18 29	bitri	|- ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! x E. y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
31		df-reu	|- ( E! y e. C E. x e. B ( x = A /\ ps ) <-> E! y ( y e. C /\ E. x e. B ( x = A /\ ps ) ) )
32		nfv	|- F/ x y e. C
33	32	r19.41	|- ( E. x e. B ( ( x = A /\ ps ) /\ y e. C ) <-> ( E. x e. B ( x = A /\ ps ) /\ y e. C ) )
34		ancom	|- ( ( y e. C /\ ( x = A /\ ps ) ) <-> ( ( x = A /\ ps ) /\ y e. C ) )
35	34	rexbii	|- ( E. x e. B ( y e. C /\ ( x = A /\ ps ) ) <-> E. x e. B ( ( x = A /\ ps ) /\ y e. C ) )
36		ancom	|- ( ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> ( E. x e. B ( x = A /\ ps ) /\ y e. C ) )
37	33 35 36	3bitr4i	|- ( E. x e. B ( y e. C /\ ( x = A /\ ps ) ) <-> ( y e. C /\ E. x e. B ( x = A /\ ps ) ) )
38		df-rex	|- ( E. x e. B ( y e. C /\ ( x = A /\ ps ) ) <-> E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
39	37 38	bitr3i	|- ( ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
40	39	eubii	|- ( E! y ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> E! y E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
41	31 40	bitri	|- ( E! y e. C E. x e. B ( x = A /\ ps ) <-> E! y E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
42	17 30 41	3imtr4g	|- ( A. x E* y ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
43	16 42	sylbi	|- ( A. x e. B E* y ( y e. C /\ ( x = A /\ ps ) ) -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
44	11 43	sylbi	|- ( A. x e. B E* y e. C ( x = A /\ ps ) -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
45	9 44	syl	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) -> E! y e. C E. x e. B ( x = A /\ ps ) ) )
46		df-ral	|- ( A. y e. C E* x ( x e. B /\ ( x = A /\ ps ) ) <-> A. y ( y e. C -> E* x ( x e. B /\ ( x = A /\ ps ) ) ) )
47		moanimv	|- ( E* x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) <-> ( y e. C -> E* x ( x e. B /\ ( x = A /\ ps ) ) ) )
48	47	albii	|- ( A. y E* x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) <-> A. y ( y e. C -> E* x ( x e. B /\ ( x = A /\ ps ) ) ) )
49	46 48	bitr4i	|- ( A. y e. C E* x ( x e. B /\ ( x = A /\ ps ) ) <-> A. y E* x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
50		2euswapv	|- ( A. y E* x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) -> ( E! y E. x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) -> E! x E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) ) )
51		r19.42v	|- ( E. x e. B ( y e. C /\ ( x = A /\ ps ) ) <-> ( y e. C /\ E. x e. B ( x = A /\ ps ) ) )
52	51 38	bitr3i	|- ( ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) )
53		an12	|- ( ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) <-> ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
54	53	exbii	|- ( E. x ( x e. B /\ ( y e. C /\ ( x = A /\ ps ) ) ) <-> E. x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
55	52 54	bitri	|- ( ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> E. x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
56	55	eubii	|- ( E! y ( y e. C /\ E. x e. B ( x = A /\ ps ) ) <-> E! y E. x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
57	31 56	bitri	|- ( E! y e. C E. x e. B ( x = A /\ ps ) <-> E! y E. x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
58	25	eubii	|- ( E! x ( x e. B /\ E. y e. C ( x = A /\ ps ) ) <-> E! x E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
59	18 58	bitri	|- ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! x E. y ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) )
60	50 57 59	3imtr4g	|- ( A. y E* x ( y e. C /\ ( x e. B /\ ( x = A /\ ps ) ) ) -> ( E! y e. C E. x e. B ( x = A /\ ps ) -> E! x e. B E. y e. C ( x = A /\ ps ) ) )
61	49 60	sylbi	|- ( A. y e. C E* x ( x e. B /\ ( x = A /\ ps ) ) -> ( E! y e. C E. x e. B ( x = A /\ ps ) -> E! x e. B E. y e. C ( x = A /\ ps ) ) )
62		moeq	|- E* x x = A
63	62	moani	|- E* x ( ( x e. B /\ ps ) /\ x = A )
64		ancom	|- ( ( ( x e. B /\ ps ) /\ x = A ) <-> ( x = A /\ ( x e. B /\ ps ) ) )
65		an12	|- ( ( x = A /\ ( x e. B /\ ps ) ) <-> ( x e. B /\ ( x = A /\ ps ) ) )
66	64 65	bitri	|- ( ( ( x e. B /\ ps ) /\ x = A ) <-> ( x e. B /\ ( x = A /\ ps ) ) )
67	66	mobii	|- ( E* x ( ( x e. B /\ ps ) /\ x = A ) <-> E* x ( x e. B /\ ( x = A /\ ps ) ) )
68	63 67	mpbi	|- E* x ( x e. B /\ ( x = A /\ ps ) )
69	68	a1i	|- ( y e. C -> E* x ( x e. B /\ ( x = A /\ ps ) ) )
70	61 69	mprg	|- ( E! y e. C E. x e. B ( x = A /\ ps ) -> E! x e. B E. y e. C ( x = A /\ ps ) )
71	45 70	impbid1	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C E. x e. B ( x = A /\ ps ) ) )
72		biidd	|- ( x = A -> ( ps <-> ps ) )
73	72	ceqsrexv	|- ( A e. B -> ( E. x e. B ( x = A /\ ps ) <-> ps ) )
74	2 73	syl	|- ( ( ph /\ y e. C ) -> ( E. x e. B ( x = A /\ ps ) <-> ps ) )
75	74	reubidva	|- ( ph -> ( E! y e. C E. x e. B ( x = A /\ ps ) <-> E! y e. C ps ) )
76	71 75	bitrd	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ps ) <-> E! y e. C ps ) )