Metamath Proof Explorer

Theorem nfriotadw

Description: Deduction version of nfriota with a disjoint variable condition, which contrary to nfriotad does not require ax-13 . (Contributed by NM, 18-Feb-2013) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 nfriotadw.1 
 |-  F/ y ph
2 nfriotadw.2 
 |-  ( ph -> F/ x ps )
3 nfriotadw.3 
 |-  ( ph -> F/_ x A )
4 df-riota 
 |-  ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
5 nfnaew 
 |-  F/ y -. A. x x = y
6 1 5 nfan 
 |-  F/ y ( ph /\ -. A. x x = y )
7 nfcvd 
 |-  ( -. 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 nfiotadw 
 |-  ( ( 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 biidd 
 |-  ( A. x x = y -> ( w e. ( iota y ( y e. A /\ ps ) ) <-> w e. ( iota y ( y e. A /\ ps ) ) ) )
17 16 drnf1v 
 |-  ( A. x x = y -> ( F/ x w e. ( iota y ( y e. A /\ ps ) ) <-> F/ y w e. ( iota y ( y e. A /\ ps ) ) ) )
18 17 albidv 
 |-  ( A. x x = y -> ( A. w F/ x w e. ( iota y ( y e. A /\ ps ) ) <-> A. w F/ y w e. ( iota y ( y e. A /\ ps ) ) ) )
19 df-nfc 
 |-  ( F/_ x ( iota y ( y e. A /\ ps ) ) <-> A. w F/ x w e. ( iota y ( y e. A /\ ps ) ) )
20 df-nfc 
 |-  ( F/_ y ( iota y ( y e. A /\ ps ) ) <-> A. w F/ y w e. ( iota y ( y e. A /\ ps ) ) )
21 18 19 20 3bitr4g 
 |-  ( A. x x = y -> ( F/_ x ( iota y ( y e. A /\ ps ) ) <-> F/_ y ( iota y ( y e. A /\ ps ) ) ) )
22 15 21 mpbiri 
 |-  ( A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) )
23 14 22 pm2.61d2 
 |-  ( ph -> F/_ x ( iota y ( y e. A /\ ps ) ) )
24 4 23 nfcxfrd 
 |-  ( ph -> F/_ x ( iota_ y e. A ps ) )