Metamath Proof Explorer


Theorem riotass2

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)

Ref Expression
Assertion riotass2 ABxAφψxAφ∃!xBψιxA|φ=ιxB|ψ

Proof

Step Hyp Ref Expression
1 reuss2 ABxAφψxAφ∃!xBψ∃!xAφ
2 simplr ABxAφψxAφ∃!xBψxAφψ
3 riotasbc ∃!xAφ[˙ιxA|φ/x]˙φ
4 riotacl ∃!xAφιxA|φA
5 rspsbc ιxA|φAxAφψ[˙ιxA|φ/x]˙φψ
6 sbcimg ιxA|φA[˙ιxA|φ/x]˙φψ[˙ιxA|φ/x]˙φ[˙ιxA|φ/x]˙ψ
7 5 6 sylibd ιxA|φAxAφψ[˙ιxA|φ/x]˙φ[˙ιxA|φ/x]˙ψ
8 4 7 syl ∃!xAφxAφψ[˙ιxA|φ/x]˙φ[˙ιxA|φ/x]˙ψ
9 3 8 mpid ∃!xAφxAφψ[˙ιxA|φ/x]˙ψ
10 1 2 9 sylc ABxAφψxAφ∃!xBψ[˙ιxA|φ/x]˙ψ
11 1 4 syl ABxAφψxAφ∃!xBψιxA|φA
12 ssel ABιxA|φAιxA|φB
13 12 ad2antrr ABxAφψxAφ∃!xBψιxA|φAιxA|φB
14 11 13 mpd ABxAφψxAφ∃!xBψιxA|φB
15 simprr ABxAφψxAφ∃!xBψ∃!xBψ
16 nfriota1 _xιxA|φ
17 16 nfsbc1 x[˙ιxA|φ/x]˙ψ
18 sbceq1a x=ιxA|φψ[˙ιxA|φ/x]˙ψ
19 16 17 18 riota2f ιxA|φB∃!xBψ[˙ιxA|φ/x]˙ψιxB|ψ=ιxA|φ
20 14 15 19 syl2anc ABxAφψxAφ∃!xBψ[˙ιxA|φ/x]˙ψιxB|ψ=ιxA|φ
21 10 20 mpbid ABxAφψxAφ∃!xBψιxB|ψ=ιxA|φ
22 21 eqcomd ABxAφψxAφ∃!xBψιxA|φ=ιxB|ψ