This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riotaprop

Description: Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013)

Ref Expression
Hypotheses riotaprop.0 
|- F/ x ps
riotaprop.1 
|- B = ( iota_ x e. A ph )
riotaprop.2 
|- ( x = B -> ( ph <-> ps ) )
Assertion riotaprop 
|- ( E! x e. A ph -> ( B e. A /\ ps ) )

Proof

Step Hyp Ref Expression
1 riotaprop.0 
 |-  F/ x ps
2 riotaprop.1 
 |-  B = ( iota_ x e. A ph )
3 riotaprop.2 
 |-  ( x = B -> ( ph <-> ps ) )
4 riotacl 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
5 2 4 eqeltrid 
 |-  ( E! x e. A ph -> B e. A )
6 2 eqcomi 
 |-  ( iota_ x e. A ph ) = B
7 nfriota1 
 |-  F/_ x ( iota_ x e. A ph )
8 2 7 nfcxfr 
 |-  F/_ x B
9 8 1 3 riota2f 
 |-  ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
10 6 9 mpbiri 
 |-  ( ( B e. A /\ E! x e. A ph ) -> ps )
11 5 10 mpancom 
 |-  ( E! x e. A ph -> ps )
12 5 11 jca 
 |-  ( E! x e. A ph -> ( B e. A /\ ps ) )