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 ⊢Ⅎ_yC
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∈Ax=B
Assertion riotaxfrd ⊢φ∧∃!x∈Aψ→ιx∈A|ψ=C

Proof

Step Hyp Ref Expression
1 riotaxfrd.1 ⊢Ⅎ_yC
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∈Ax=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∈Ax∈x∈A|ψ
27 26 biimpi ⊢∃!x∈Aψ→∃!x∈Ax∈x∈A|ψ
28 27 adantl ⊢φ∧∃!x∈Aψ→∃!x∈Ax∈x∈A|ψ
29 nfcv ⊢Ⅎ_xC
30 nfrab1 ⊢Ⅎ_xx∈A|ψ
31 30 nfel2 ⊢ℲxC∈x∈A|ψ
32 eleq1 ⊢x=C→x∈x∈A|ψ↔C∈x∈A|ψ
33 29 31 32 riota2f ⊢C∈A∧∃!x∈Ax∈x∈A|ψ→C∈x∈A|ψ↔ιx∈A|x∈x∈A|ψ=C
34 24 28 33 syl2anc ⊢φ∧∃!x∈Aψ→C∈x∈A|ψ↔ιx∈A|x∈x∈A|ψ=C
35 20 34 mpbid ⊢φ∧∃!x∈Aψ→ιx∈A|x∈x∈A|ψ=C
36 9 35 eqtr3id ⊢φ∧∃!x∈Aψ→ιx∈A|ψ=C