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	bilani	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
28		nfcv	⊢ Ⅎ 𝑥 𝐶
29		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜓 }
30	29	nfel2	⊢ Ⅎ 𝑥 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 }
31		eleq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) )
32	28 30 31	riota2f	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( ℩ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = 𝐶 ) )
33	24 27 32	syl2anc	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( ℩ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = 𝐶 ) )
34	20 33	mpbid	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( ℩ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = 𝐶 )
35	9 34	eqtr3id	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ( ℩ 𝑥 ∈ 𝐴 𝜓 ) = 𝐶 )