Metamath Proof Explorer

Theorem riotaxfrd

Description: Change the variable x in the expression for "the unique x such that ps " to another variable y contained in expression B . Use reuhypd to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riotaxfrd.1 ⊢ Ⅎ _ y C
riotaxfrd.2 ⊢ φ ∧ y ∈ A → B ∈ A
riotaxfrd.3 ⊢ φ ∧ ι y ∈ A | χ ∈ A → C ∈ A
riotaxfrd.4 ⊢ x = B → ψ ↔ χ
riotaxfrd.5 ⊢ y = ι y ∈ A | χ → B = C
riotaxfrd.6 ⊢ φ ∧ x ∈ A → ∃! y ∈ A x = B
Assertion riotaxfrd ⊢ φ ∧ ∃! x ∈ A ψ → ι x ∈ A | ψ = C

Proof

Step Hyp Ref Expression
1 riotaxfrd.1 ⊢ Ⅎ _ y C
2 riotaxfrd.2 ⊢ φ ∧ y ∈ A → B ∈ A
3 riotaxfrd.3 ⊢ φ ∧ ι y ∈ A | χ ∈ A → C ∈ A
4 riotaxfrd.4 ⊢ x = B → ψ ↔ χ
5 riotaxfrd.5 ⊢ y = ι y ∈ A | χ → B = C
6 riotaxfrd.6 ⊢ φ ∧ x ∈ A → ∃! y ∈ A x = B
7 rabid ⊢ x ∈ x ∈ A | ψ ↔ x ∈ A ∧ ψ
8 7 baib ⊢ x ∈ A → x ∈ x ∈ A | ψ ↔ ψ
9 8 riotabiia ⊢ ι x ∈ A | x ∈ x ∈ A | ψ = ι x ∈ A | ψ
10 2 6 4 reuxfr1ds ⊢ φ → ∃! x ∈ A ψ ↔ ∃! y ∈ A χ
11 riotacl2 ⊢ ∃! y ∈ A χ → ι y ∈ A | χ ∈ y ∈ A | χ
12 11 adantl ⊢ φ ∧ ∃! y ∈ A χ → ι y ∈ A | χ ∈ y ∈ A | χ
13 riotacl ⊢ ∃! y ∈ A χ → ι y ∈ A | χ ∈ A
14 nfriota1 ⊢ Ⅎ _ y ι y ∈ A | χ
15 14 1 2 4 5 rabxfrd ⊢ φ ∧ ι y ∈ A | χ ∈ A → C ∈ x ∈ A | ψ ↔ ι y ∈ A | χ ∈ y ∈ A | χ
16 13 15 sylan2 ⊢ φ ∧ ∃! y ∈ A χ → C ∈ x ∈ A | ψ ↔ ι y ∈ A | χ ∈ y ∈ A | χ
17 12 16 mpbird ⊢ φ ∧ ∃! y ∈ A χ → C ∈ x ∈ A | ψ
18 17 ex ⊢ φ → ∃! y ∈ A χ → C ∈ x ∈ A | ψ
19 10 18 sylbid ⊢ φ → ∃! x ∈ A ψ → C ∈ x ∈ A | ψ
20 19 imp ⊢ φ ∧ ∃! x ∈ A ψ → C ∈ x ∈ A | ψ
21 3 ex ⊢ φ → ι y ∈ A | χ ∈ A → C ∈ A
22 13 21 syl5 ⊢ φ → ∃! y ∈ A χ → C ∈ A
23 10 22 sylbid ⊢ φ → ∃! x ∈ A ψ → C ∈ A
24 23 imp ⊢ φ ∧ ∃! x ∈ A ψ → C ∈ A
25 7 baibr ⊢ x ∈ A → ψ ↔ x ∈ x ∈ A | ψ
26 25 reubiia ⊢ ∃! x ∈ A ψ ↔ ∃! x ∈ A x ∈ x ∈ A | ψ
27 26 bilani ⊢ φ ∧ ∃! x ∈ A ψ → ∃! x ∈ A x ∈ x ∈ A | ψ
28 nfcv ⊢ Ⅎ _ x C
29 nfrab1 ⊢ Ⅎ _ x x ∈ A | ψ
30 29 nfel2 ⊢ Ⅎ x C ∈ x ∈ A | ψ
31 eleq1 ⊢ x = C → x ∈ x ∈ A | ψ ↔ C ∈ x ∈ A | ψ
32 28 30 31 riota2f ⊢ C ∈ A ∧ ∃! x ∈ A x ∈ x ∈ A | ψ → C ∈ x ∈ A | ψ ↔ ι x ∈ A | x ∈ x ∈ A | ψ = C
33 24 27 32 syl2anc ⊢ φ ∧ ∃! x ∈ A ψ → C ∈ x ∈ A | ψ ↔ ι x ∈ A | x ∈ x ∈ A | ψ = C
34 20 33 mpbid ⊢ φ ∧ ∃! x ∈ A ψ → ι x ∈ A | x ∈ x ∈ A | ψ = C
35 9 34 eqtr3id ⊢ φ ∧ ∃! x ∈ A ψ → ι x ∈ A | ψ = C