Theorem reuxfr2 2909

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

Hypotheses

Ref	Expression
reuxfr2.1	⊢ (y ∈ B → A ∈ B)
reuxfr2.2	⊢ (x ∈ B → ∃*y(y ∈ B ⋀ x = A))

Assertion

Ref	Expression
reuxfr2	⊢ (∃!x ∈ B ∃y ∈ B (x = A ⋀ φ) ↔ ∃!y ∈ B φ)

Distinct variable groups:   φ,x   x,A   x,y,B

Proof of Theorem reuxfr2

Step	Hyp	Ref	Expression
1		2reuswap 1940	. . . 4 ⊢ (∀x ∈ B ∃*y(y ∈ B ⋀ (x = A ⋀ φ)) → (∃!x ∈ B ∃y ∈ B (x = A ⋀ φ) → ∃!y ∈ B ∃x ∈ B (x = A ⋀ φ)))
2		reuxfr2.2	. . . . . 6 ⊢ (x ∈ B → ∃*y(y ∈ B ⋀ x = A))
3		moan 1424	. . . . . 6 ⊢ (∃*y(y ∈ B ⋀ x = A) → ∃*y(φ ⋀ (y ∈ B ⋀ x = A)))
4	2, 3	syl 10	. . . . 5 ⊢ (x ∈ B → ∃*y(φ ⋀ (y ∈ B ⋀ x = A)))
5		ancom 437	. . . . . . 7 ⊢ ((φ ⋀ (y ∈ B ⋀ x = A)) ↔ ((y ∈ B ⋀ x = A) ⋀ φ))
6		anass 441	. . . . . . 7 ⊢ (((y ∈ B ⋀ x = A) ⋀ φ) ↔ (y ∈ B ⋀ (x = A ⋀ φ)))
7	5, 6	bitr 173	. . . . . 6 ⊢ ((φ ⋀ (y ∈ B ⋀ x = A)) ↔ (y ∈ B ⋀ (x = A ⋀ φ)))
8	7	mobii 1407	. . . . 5 ⊢ (∃*y(φ ⋀ (y ∈ B ⋀ x = A)) ↔ ∃*y(y ∈ B ⋀ (x = A ⋀ φ)))
9	4, 8	sylib 198	. . . 4 ⊢ (x ∈ B → ∃*y(y ∈ B ⋀ (x = A ⋀ φ)))
10	1, 9	mprg 1703	. . 3 ⊢ (∃!x ∈ B ∃y ∈ B (x = A ⋀ φ) → ∃!y ∈ B ∃x ∈ B (x = A ⋀ φ))
11		2reuswap 1940	. . . 4 ⊢ (∀y ∈ B ∃*x(x ∈ B ⋀ (x = A ⋀ φ)) → (∃!y ∈ B ∃x ∈ B (x = A ⋀ φ) → ∃!x ∈ B ∃y ∈ B (x = A ⋀ φ)))
12		moeq 1923	. . . . . . 7 ⊢ ∃*x x = A
13	12	moani 1425	. . . . . 6 ⊢ ∃*x((x ∈ B ⋀ φ) ⋀ x = A)
14		ancom 437	. . . . . . . 8 ⊢ (((x ∈ B ⋀ φ) ⋀ x = A) ↔ (x = A ⋀ (x ∈ B ⋀ φ)))
15		an12 486	. . . . . . . 8 ⊢ ((x = A ⋀ (x ∈ B ⋀ φ)) ↔ (x ∈ B ⋀ (x = A ⋀ φ)))
16	14, 15	bitr 173	. . . . . . 7 ⊢ (((x ∈ B ⋀ φ) ⋀ x = A) ↔ (x ∈ B ⋀ (x = A ⋀ φ)))
17	16	mobii 1407	. . . . . 6 ⊢ (∃*x((x ∈ B ⋀ φ) ⋀ x = A) ↔ ∃*x(x ∈ B ⋀ (x = A ⋀ φ)))
18	13, 17	mpbi 189	. . . . 5 ⊢ ∃*x(x ∈ B ⋀ (x = A ⋀ φ))
19	18	a1i 8	. . . 4 ⊢ (y ∈ B → ∃*x(x ∈ B ⋀ (x = A ⋀ φ)))
20	11, 19	mprg 1703	. . 3 ⊢ (∃!y ∈ B ∃x ∈ B (x = A ⋀ φ) → ∃!x ∈ B ∃y ∈ B (x = A ⋀ φ))
21	10, 20	impbi 157	. 2 ⊢ (∃!x ∈ B ∃y ∈ B (x = A ⋀ φ) ↔ ∃!y ∈ B ∃x ∈ B (x = A ⋀ φ))
22		reuxfr2.1	. . . 4 ⊢ (y ∈ B → A ∈ B)
23		pm4.2d 171	. . . . 5 ⊢ (x = A → (φ ↔ φ))
24	23	ceqsrexv 1892	. . . 4 ⊢ (A ∈ B → (∃x ∈ B (x = A ⋀ φ) ↔ φ))
25	22, 24	syl 10	. . 3 ⊢ (y ∈ B → (∃x ∈ B (x = A ⋀ φ) ↔ φ))
26	25	reubiia 1784	. 2 ⊢ (∃!y ∈ B ∃x ∈ B (x = A ⋀ φ) ↔ ∃!y ∈ B φ)
27	21, 26	bitr 173	1 ⊢ (∃!x ∈ B ∃y ∈ B (x = A ⋀ φ) ↔ ∃!y ∈ B φ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∃*wmo 1383  ∃wrex 1649  ∃!wreu 1650

This theorem is referenced by:  reuxfr 2910

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-rex 1653  df-reu 1654  df-v 1815

Copyright terms: Public domain