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

Metamath Proof Explorer

Theorem nfriotad

Description: Deduction version of nfriota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfriotadw when possible. (Contributed by NM, 18-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfriotad.1 
|- F/ y ph
nfriotad.2 
|- ( ph -> F/ x ps )
nfriotad.3 
|- ( ph -> F/_ x A )
Assertion nfriotad 
|- ( ph -> F/_ x ( iota_ y e. A ps ) )

Proof

Step Hyp Ref Expression
1 nfriotad.1 
 |-  F/ y ph
2 nfriotad.2 
 |-  ( ph -> F/ x ps )
3 nfriotad.3 
 |-  ( ph -> F/_ x A )
4 df-riota 
 |-  ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
5 nfnae 
 |-  F/ y -. A. x x = y
6 1 5 nfan 
 |-  F/ y ( ph /\ -. A. x x = y )
7 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
8 7 adantl 
 |-  ( ( ph /\ -. A. x x = y ) -> F/_ x y )
9 3 adantr 
 |-  ( ( ph /\ -. A. x x = y ) -> F/_ x A )
10 8 9 nfeld 
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x y e. A )
11 2 adantr 
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x ps )
12 10 11 nfand 
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x ( y e. A /\ ps ) )
13 6 12 nfiotad 
 |-  ( ( ph /\ -. A. x x = y ) -> F/_ x ( iota y ( y e. A /\ ps ) ) )
14 13 ex 
 |-  ( ph -> ( -. A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) ) )
15 nfiota1 
 |-  F/_ y ( iota y ( y e. A /\ ps ) )
16 eqidd 
 |-  ( A. x x = y -> ( iota y ( y e. A /\ ps ) ) = ( iota y ( y e. A /\ ps ) ) )
17 16 drnfc1 
 |-  ( A. x x = y -> ( F/_ x ( iota y ( y e. A /\ ps ) ) <-> F/_ y ( iota y ( y e. A /\ ps ) ) ) )
18 15 17 mpbiri 
 |-  ( A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) )
19 14 18 pm2.61d2 
 |-  ( ph -> F/_ x ( iota y ( y e. A /\ ps ) ) )
20 4 19 nfcxfrd 
 |-  ( ph -> F/_ x ( iota_ y e. A ps ) )