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 ) )