Theorem reuxfr2d 3844

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A.

Hypotheses

Ref	Expression
reuxfr2d.1	|- ((ph /\ y e. B) -> A e. B)
reuxfr2d.2	|- ((ph /\ x e. B) -> E*y(y e. B /\ x = A))

Assertion

Ref	Expression
reuxfr2d	|- (ph -> (E!x e. B E.y e. B (x = A /\ ps) <-> E!y e. B ps))

Distinct variable groups:   x,y,ph   ps,x   x,A   x,B,y

Proof of Theorem reuxfr2d

Step	Hyp	Ref	Expression
1		reuxfr2d.2	. . . . . . 7 |- ((ph /\ x e. B) -> E*y(y e. B /\ x = A))
2		moan 1819	. . . . . . 7 |- (E*y(y e. B /\ x = A) -> E*y(ps /\ (y e. B /\ x = A)))
3	1, 2	syl 12	. . . . . 6 |- ((ph /\ x e. B) -> E*y(ps /\ (y e. B /\ x = A)))
4		ancom 482	. . . . . . . 8 |- ((ps /\ (y e. B /\ x = A)) <-> ((y e. B /\ x = A) /\ ps))
5		anass 487	. . . . . . . 8 |- (((y e. B /\ x = A) /\ ps) <-> (y e. B /\ (x = A /\ ps)))
6	4, 5	bitri 190	. . . . . . 7 |- ((ps /\ (y e. B /\ x = A)) <-> (y e. B /\ (x = A /\ ps)))
7	6	mobii 1801	. . . . . 6 |- (E*y(ps /\ (y e. B /\ x = A)) <-> E*y(y e. B /\ (x = A /\ ps)))
8	3, 7	sylib 215	. . . . 5 |- ((ph /\ x e. B) -> E*y(y e. B /\ (x = A /\ ps)))
9	8	r19.21aiva 2176	. . . 4 |- (ph -> A.x e. B E*y(y e. B /\ (x = A /\ ps)))
10		2reuswap 2449	. . . 4 |- (A.x e. B E*y(y e. B /\ (x = A /\ ps)) -> (E!x e. B E.y e. B (x = A /\ ps) -> E!y e. B E.x e. B (x = A /\ ps)))
11	9, 10	syl 12	. . 3 |- (ph -> (E!x e. B E.y e. B (x = A /\ ps) -> E!y e. B E.x e. B (x = A /\ ps)))
12		2reuswap 2449	. . . 4 |- (A.y e. B E*x(x e. B /\ (x = A /\ ps)) -> (E!y e. B E.x e. B (x = A /\ ps) -> E!x e. B E.y e. B (x = A /\ ps)))
13		moeq 2431	. . . . . . 7 |- E*x x = A
14	13	moani 1820	. . . . . 6 |- E*x((x e. B /\ ps) /\ x = A)
15		ancom 482	. . . . . . . 8 |- (((x e. B /\ ps) /\ x = A) <-> (x = A /\ (x e. B /\ ps)))
16		an12 542	. . . . . . . 8 |- ((x = A /\ (x e. B /\ ps)) <-> (x e. B /\ (x = A /\ ps)))
17	15, 16	bitri 190	. . . . . . 7 |- (((x e. B /\ ps) /\ x = A) <-> (x e. B /\ (x = A /\ ps)))
18	17	mobii 1801	. . . . . 6 |- (E*x((x e. B /\ ps) /\ x = A) <-> E*x(x e. B /\ (x = A /\ ps)))
19	14, 18	mpbi 206	. . . . 5 |- E*x(x e. B /\ (x = A /\ ps))
20	19	a1i 8	. . . 4 |- (y e. B -> E*x(x e. B /\ (x = A /\ ps)))
21	12, 20	mprg 2162	. . 3 |- (E!y e. B E.x e. B (x = A /\ ps) -> E!x e. B E.y e. B (x = A /\ ps))
22	11, 21	impbid1 575	. 2 |- (ph -> (E!x e. B E.y e. B (x = A /\ ps) <-> E!y e. B E.x e. B (x = A /\ ps)))
23		reuxfr2d.1	. . . 4 |- ((ph /\ y e. B) -> A e. B)
24		biidd 188	. . . . 5 |- (x = A -> (ps <-> ps))
25	24	ceqsrexv 2394	. . . 4 |- (A e. B -> (E.x e. B (x = A /\ ps) <-> ps))
26	23, 25	syl 12	. . 3 |- ((ph /\ y e. B) -> (E.x e. B (x = A /\ ps) <-> ps))
27	26	reubidva 2259	. 2 |- (ph -> (E!y e. B E.x e. B (x = A /\ ps) <-> E!y e. B ps))
28	22, 27	bitrd 587	1 |- (ph -> (E!x e. B E.y e. B (x = A /\ ps) <-> E!y e. B ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E*wmo 1772  A.wral 2105  E.wrex 2106  E!wreu 2107

This theorem is referenced by:  reuxfrd 3846

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-reu 2111  df-v 2294

Copyright terms: Public domain