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 𝑦 𝐶
riotaxfrd.2 ( ( 𝜑𝑦𝐴 ) → 𝐵𝐴 )
riotaxfrd.3 ( ( 𝜑 ∧ ( 𝑦𝐴 𝜒 ) ∈ 𝐴 ) → 𝐶𝐴 )
riotaxfrd.4 ( 𝑥 = 𝐵 → ( 𝜓𝜒 ) )
riotaxfrd.5 ( 𝑦 = ( 𝑦𝐴 𝜒 ) → 𝐵 = 𝐶 )
riotaxfrd.6 ( ( 𝜑𝑥𝐴 ) → ∃! 𝑦𝐴 𝑥 = 𝐵 )
Assertion riotaxfrd ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → ( 𝑥𝐴 𝜓 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 riotaxfrd.1 𝑦 𝐶
2 riotaxfrd.2 ( ( 𝜑𝑦𝐴 ) → 𝐵𝐴 )
3 riotaxfrd.3 ( ( 𝜑 ∧ ( 𝑦𝐴 𝜒 ) ∈ 𝐴 ) → 𝐶𝐴 )
4 riotaxfrd.4 ( 𝑥 = 𝐵 → ( 𝜓𝜒 ) )
5 riotaxfrd.5 ( 𝑦 = ( 𝑦𝐴 𝜒 ) → 𝐵 = 𝐶 )
6 riotaxfrd.6 ( ( 𝜑𝑥𝐴 ) → ∃! 𝑦𝐴 𝑥 = 𝐵 )
7 rabid ( 𝑥 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑥𝐴𝜓 ) )
8 7 baib ( 𝑥𝐴 → ( 𝑥 ∈ { 𝑥𝐴𝜓 } ↔ 𝜓 ) )
9 8 riotabiia ( 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } ) = ( 𝑥𝐴 𝜓 )
10 2 6 4 reuxfr1ds ( 𝜑 → ( ∃! 𝑥𝐴 𝜓 ↔ ∃! 𝑦𝐴 𝜒 ) )
11 riotacl2 ( ∃! 𝑦𝐴 𝜒 → ( 𝑦𝐴 𝜒 ) ∈ { 𝑦𝐴𝜒 } )
12 11 adantl ( ( 𝜑 ∧ ∃! 𝑦𝐴 𝜒 ) → ( 𝑦𝐴 𝜒 ) ∈ { 𝑦𝐴𝜒 } )
13 riotacl ( ∃! 𝑦𝐴 𝜒 → ( 𝑦𝐴 𝜒 ) ∈ 𝐴 )
14 nfriota1 𝑦 ( 𝑦𝐴 𝜒 )
15 14 1 2 4 5 rabxfrd ( ( 𝜑 ∧ ( 𝑦𝐴 𝜒 ) ∈ 𝐴 ) → ( 𝐶 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑦𝐴 𝜒 ) ∈ { 𝑦𝐴𝜒 } ) )
16 13 15 sylan2 ( ( 𝜑 ∧ ∃! 𝑦𝐴 𝜒 ) → ( 𝐶 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑦𝐴 𝜒 ) ∈ { 𝑦𝐴𝜒 } ) )
17 12 16 mpbird ( ( 𝜑 ∧ ∃! 𝑦𝐴 𝜒 ) → 𝐶 ∈ { 𝑥𝐴𝜓 } )
18 17 ex ( 𝜑 → ( ∃! 𝑦𝐴 𝜒𝐶 ∈ { 𝑥𝐴𝜓 } ) )
19 10 18 sylbid ( 𝜑 → ( ∃! 𝑥𝐴 𝜓𝐶 ∈ { 𝑥𝐴𝜓 } ) )
20 19 imp ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → 𝐶 ∈ { 𝑥𝐴𝜓 } )
21 3 ex ( 𝜑 → ( ( 𝑦𝐴 𝜒 ) ∈ 𝐴𝐶𝐴 ) )
22 13 21 syl5 ( 𝜑 → ( ∃! 𝑦𝐴 𝜒𝐶𝐴 ) )
23 10 22 sylbid ( 𝜑 → ( ∃! 𝑥𝐴 𝜓𝐶𝐴 ) )
24 23 imp ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → 𝐶𝐴 )
25 7 baibr ( 𝑥𝐴 → ( 𝜓𝑥 ∈ { 𝑥𝐴𝜓 } ) )
26 25 reubiia ( ∃! 𝑥𝐴 𝜓 ↔ ∃! 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } )
27 26 biimpi ( ∃! 𝑥𝐴 𝜓 → ∃! 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } )
28 27 adantl ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → ∃! 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } )
29 nfcv 𝑥 𝐶
30 nfrab1 𝑥 { 𝑥𝐴𝜓 }
31 30 nfel2 𝑥 𝐶 ∈ { 𝑥𝐴𝜓 }
32 eleq1 ( 𝑥 = 𝐶 → ( 𝑥 ∈ { 𝑥𝐴𝜓 } ↔ 𝐶 ∈ { 𝑥𝐴𝜓 } ) )
33 29 31 32 riota2f ( ( 𝐶𝐴 ∧ ∃! 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } ) → ( 𝐶 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } ) = 𝐶 ) )
34 24 28 33 syl2anc ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → ( 𝐶 ∈ { 𝑥𝐴𝜓 } ↔ ( 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } ) = 𝐶 ) )
35 20 34 mpbid ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → ( 𝑥𝐴 𝑥 ∈ { 𝑥𝐴𝜓 } ) = 𝐶 )
36 9 35 eqtr3id ( ( 𝜑 ∧ ∃! 𝑥𝐴 𝜓 ) → ( 𝑥𝐴 𝜓 ) = 𝐶 )